Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. canonical multiplicative euclidean size
  2. clarified parity
  3. clarified uniqueness criterion for euclidean rings
  4. tuned proofs
  5. tuned imports
Changeset 66840:0d689d71dbdc by haftmann:
canonical multiplicative euclidean size
The file was modified src/HOL/Computational_Algebra/Polynomial_Factorial.thy (diff)
The file was modified src/HOL/Euclidean_Division.thy (diff)
The file was modified src/HOL/Parity.thy (diff)
Changeset 66839:909ba5ed93dd by haftmann:
clarified parity
The file was modified src/HOL/Code_Numeral.thy (diff)
The file was modified src/HOL/Euclidean_Division.thy (diff)
The file was modified src/HOL/Parity.thy (diff)
Changeset 66838:17989f6bc7b2 by haftmann:
clarified uniqueness criterion for euclidean rings
The file was modified src/HOL/Code_Numeral.thy (diff)
The file was modified src/HOL/Computational_Algebra/Field_as_Ring.thy (diff)
The file was modified src/HOL/Computational_Algebra/Polynomial_Factorial.thy (diff)
The file was modified src/HOL/Enum.thy (diff)
The file was modified src/HOL/Euclidean_Division.thy (diff)
Changeset 66837:6ba663ff2b1c by haftmann:
tuned proofs
The file was modified src/HOL/Computational_Algebra/Primes.thy (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/Library/Infinite_Set.thy (diff)
The file was modified src/HOL/Number_Theory/Cong.thy (diff)
The file was modified src/HOL/Number_Theory/Quadratic_Reciprocity.thy (diff)
The file was modified src/HOL/Number_Theory/Residues.thy (diff)
Changeset 66836:4eb431c3f974 by haftmann:
tuned imports
The file was modified src/HOL/Code_Numeral.thy (diff)
The file was modified src/HOL/GCD.thy (diff)
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/Int.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/Nat_Transfer.thy (diff)
The file was modified src/HOL/Semiring_Normalization.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)