Changes

Summary

dedicated definition for coprimality
more induct rules on nat

Changeset 67051:e7e54a0b9197 by haftmann: dedicated definition for coprimality
The file was modified	`NEWS` (diff)
The file was modified	`src/Doc/Corec/Corec.thy` (diff)
The file was modified	`src/HOL/Algebra/Multiplicative_Group.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Factorial_Ring.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Normalized_Fraction.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Nth_Powers.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Polynomial_Factorial.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Primes.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Squarefree.thy` (diff)
The file was modified	`src/HOL/Corec_Examples/Paper_Examples.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Rat_Pair.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/Isar_Examples/Fibonacci.thy` (diff)
The file was modified	`src/HOL/Library/Multiset.thy` (diff)
The file was modified	`src/HOL/Map.thy` (diff)
The file was modified	`src/HOL/Nitpick.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Cong.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Euler_Criterion.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Fib.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/Residues.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Totient.thy` (diff)
The file was modified	`src/HOL/Parity.thy` (diff)
The file was modified	`src/HOL/Rat.thy` (diff)
The file was modified	`src/HOL/Real.thy` (diff)
The file was modified	`src/HOL/Rings.thy` (diff)
The file was modified	`src/HOL/Set.thy` (diff)
Changeset 67050:1e29e2666a15 by haftmann: more induct rules on nat
The file was modified	`src/HOL/Nat.thy` (diff)