Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned NEWS
  2. reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
  3. moved euclidean ring to HOL
  4. reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
Changeset 64787:067cacdd1117 by haftmann:
tuned NEWS
The file was modified NEWS (diff)
Changeset 64786:340db65fd2c1 by haftmann:
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
The file was modified NEWS (diff)
The file was modified src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy (diff)
The file was modified src/HOL/Library/Field_as_Ring.thy (diff)
The file was modified src/HOL/Library/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Library/Polynomial_Factorial.thy (diff)
The file was modified src/HOL/Number_Theory/Euclidean_Algorithm.thy (diff)
Changeset 64785:ae0bbc8e45ad by haftmann:
moved euclidean ring to HOL
The file was addedsrc/HOL/Euclidean_Division.thy
The file was modified NEWS (diff)
The file was modified src/HOL/Divides.thy (diff)
The file was modified src/HOL/Number_Theory/Euclidean_Algorithm.thy (diff)
The file was modified src/HOL/Parity.thy (diff)
The file was removedsrc/HOL/Number_Theory/Euclidean_Division.thy
Changeset 64784:5cb5e7ecb284 by haftmann:
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
The file was addedsrc/HOL/Number_Theory/Euclidean_Division.thy
The file was modified src/HOL/Library/Field_as_Ring.thy (diff)
The file was modified src/HOL/Library/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Library/Polynomial_Factorial.thy (diff)
The file was modified src/HOL/Number_Theory/Euclidean_Algorithm.thy (diff)