src/HOL/Library/Field_as_Ring.thy
2017-01-04 haftmann 2017-01-04 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
2017-01-04 haftmann 2017-01-04 reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
2016-12-17 haftmann 2016-12-17 restructured matter on polynomials and normalized fractions