Changes

Summary

more simplification rules
overhauling of primes
cleaned up and tuned
generalized more lemmas

Changeset 67118:ccab07d1196c by haftmann: more simplification rules
The file was modified	`src/HOL/Algebra/IntRing.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Primes.thy` (diff)
The file was modified	`src/HOL/Data_Structures/RBT_Set.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Ferrack.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/MIR.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/cooper_tac.ML` (diff)
The file was modified	`src/HOL/Decision_Procs/mir_tac.ML` (diff)
The file was modified	`src/HOL/Divides.thy` (diff)
The file was modified	`src/HOL/Euclidean_Division.thy` (diff)
The file was modified	`src/HOL/GCD.thy` (diff)
The file was modified	`src/HOL/Int.thy` (diff)
The file was modified	`src/HOL/Library/Float.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Euler_Criterion.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Gauss.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Quadratic_Reciprocity.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Totient.thy` (diff)
The file was modified	`src/HOL/Tools/Qelim/cooper.ML` (diff)
The file was modified	`src/HOL/Word/Word.thy` (diff)
The file was modified	`src/HOL/ex/Transfer_Int_Nat.thy` (diff)
Changeset 67117:19f627407264 by haftmann: overhauling of primes
The file was modified	`src/HOL/Computational_Algebra/Primes.thy` (diff)
Changeset 67116:7397a6df81d8 by haftmann: cleaned up and tuned
The file was modified	`src/HOL/Int.thy` (diff)
The file was modified	`src/HOL/Num.thy` (diff)
The file was modified	`src/HOL/Tools/int_arith.ML` (diff)
Changeset 67115:2977773a481c by haftmann: generalized more lemmas
The file was modified	`src/HOL/Number_Theory/Cong.thy` (diff)