src/HOL/Number_Theory/Euclidean_Algorithm.thy
2015-07-08 haftmann 2015-07-08 eliminated some duplication
2015-07-08 haftmann 2015-07-08 more algebraic properties for gcd/lcm
2015-07-08 haftmann 2015-07-08 moved normalization and unit_factor into Main HOL corpus
2015-07-02 haftmann 2015-07-02 separate (semi)ring with normalization
2015-06-27 haftmann 2015-06-27 simplified termination criterion for euclidean algorithm (again)
2015-06-27 haftmann 2015-06-27 tuned proof
2015-06-27 haftmann 2015-06-27 rings follow immediately their corresponding semirings
2015-06-25 wenzelm 2015-06-25 merged
2015-06-25 wenzelm 2015-06-25 tuned proofs;
2015-06-25 haftmann 2015-06-25 streamlined definitions and primitive lemma of euclidean algorithm, including code generation
2015-06-25 haftmann 2015-06-25 euclidean algorithm on polynomials
2015-06-25 haftmann 2015-06-25 generalized to definition from literature, which covers also polynomials
2015-06-19 wenzelm 2015-06-19 isabelle update_cartouches;
2015-06-19 haftmann 2015-06-19 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
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)