Changes

Summary

Removed redundant material related to primes
Merged
Tuned primes
Overhaul of prime/multiplicity/prime_factors

Changeset 63537:831816778409 by eberlm _eberlm@in.tum.de_: Removed redundant material related to primes
The file was modified	`src/HOL/Algebra/Exponent.thy` (diff)
The file was modified	`src/HOL/Algebra/Sylow.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Factorial_Ring.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Residues.thy` (diff)
The file was modified	`src/HOL/Proofs/Extraction/Euclid.thy` (diff)
The file was modified	`src/HOL/ROOT` (diff)
The file was removed	`src/HOL/Number_Theory/UniqueFactorization.thy`
Changeset 63536:8cecf0100996 by eberlm _eberlm@in.tum.de_: Merged
Changeset 63535:6887fda4541a by eberlm _eberlm@in.tum.de_: Tuned primes
The file was modified	`src/HOL/Number_Theory/Primes.thy` (diff)
Changeset 63534:523b488b15c9 by eberlm _eberlm@in.tum.de_: Overhaul of prime/multiplicity/prime_factors
The file was modified	`src/HOL/Algebra/Exponent.thy` (diff)
The file was modified	`src/HOL/Algebra/IntRing.thy` (diff)
The file was modified	`src/HOL/Algebra/Sylow.thy` (diff)
The file was modified	`src/HOL/Library/Multiset.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Eratosthenes.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Factorial_Ring.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Gauss.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Pocklington.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Primes.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Residues.thy` (diff)
The file was modified	`src/HOL/Number_Theory/UniqueFactorization.thy` (diff)
The file was modified	`src/HOL/Proofs/Extraction/Euclid.thy` (diff)
The file was modified	`src/HOL/ex/Sqrt.thy` (diff)
The file was modified	`src/HOL/ex/Sqrt_Script.thy` (diff)