src/HOL/Number_Theory/Euclidean_Algorithm.thy
2015-06-19 haftmann 2015-06-19 generalized some theorems about integral domains and moved to HOL theories
2015-06-12 haftmann 2015-06-12 proper subclass instances for existing gcd (semi)rings
2015-06-12 haftmann 2015-06-12 slight preference for American English
2015-06-12 haftmann 2015-06-12 generalized euclidean ring prerequisites
2015-06-12 haftmann 2015-06-12 simplified relationship between associated and is_unit
2015-06-12 haftmann 2015-06-12 tuned lemmas and proofs
2015-06-12 haftmann 2015-06-12 given up trivial definition
2015-06-12 haftmann 2015-06-12 dropped warnings by dropping ineffective code declarations
2015-06-12 haftmann 2015-06-12 standardized algebraic conventions: prefer a, b, c over x, y, z
2014-11-26 haftmann 2014-11-26 prefer abbrev for is_unit
2014-11-17 haftmann 2014-11-17 generalized lemmas and tuned proofs
2014-11-17 haftmann 2014-11-17 generalized lemmas (particularly concerning dvd) as far as appropriate
2014-11-09 haftmann 2014-11-09 self-contained simp rules for dvd on numerals
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-08-22 haftmann 2014-08-22 generic euclidean algorithm (due to Manuel Eberl)