src/HOL/Number_Theory/Euclidean_Algorithm.thy
2017-01-17 wenzelm 2017-01-17 isabelle update_cartouches -c -t;
2017-01-09 haftmann 2017-01-09 gcd/lcm on finite sets
2017-01-09 haftmann 2017-01-09 slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
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 moved euclidean ring to HOL
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 more fine-grained type class hierarchy for div and mod
2016-10-16 haftmann 2016-10-16 eliminated irregular aliasses
2016-10-16 haftmann 2016-10-16 more standardized theorem names for facts involving the div and mod identity
2016-10-16 haftmann 2016-10-16 more standardized names
2016-10-12 haftmann 2016-10-12 more standard naming convention
2016-10-12 haftmann 2016-10-12 separate type class for arbitrary quotient and remainder partitions
2016-10-11 haftmann 2016-10-11 stripped dependency on pragmatic type class semiring_div
2016-09-26 haftmann 2016-09-26 more lemmas
2016-09-18 haftmann 2016-09-18 more generic algebraic lemmas
2016-08-08 eberlm 2016-08-08 is_prime -> prime
2016-07-13 eberlm 2016-07-13 Reformed factorial rings
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-02-28 Manuel Eberl 2016-02-28 Minor adjustments to euclidean rings
2016-02-28 Manuel Eberl 2016-02-28 More efficient Extended Euclidean Algorithm
2016-02-26 Manuel Eberl 2016-02-26 Tuned Euclidean Rings/GCD rings
2016-02-26 Manuel Eberl 2016-02-26 Fixed code equations for Gcd/Lcm
2016-02-26 eberlm 2016-02-26 Tuned Euclidean Ring instance for polynomials
2016-02-25 eberlm 2016-02-25 Tuned Euclidean rings
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings and tuned proofs
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-07-08 haftmann 2015-07-08 tuned facts
2015-07-08 haftmann 2015-07-08 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
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)