src/HOL/GCD.thy
23 months ago haftmann 2017-10-08 more fundamental definition of div and mod on int
23 months ago haftmann 2017-10-08 avoid trivial definition
23 months ago haftmann 2017-10-08 tuned proofs
2017-05-11 haftmann 2017-05-11 more lemmas
2017-04-23 haftmann 2017-04-23 include GCD as integral part of computational algebra in session HOL
2017-04-22 wenzelm 2017-04-22 theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
2017-01-09 haftmann 2017-01-09 gcd/lcm on finite sets
2016-12-17 haftmann 2016-12-17 restructured matter on polynomials and normalized fractions
2016-10-17 nipkow 2016-10-17 setprod -> prod
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-09-18 haftmann 2016-09-18 more generic algebraic lemmas
2016-09-18 wenzelm 2016-09-18 tuned proofs;
2016-09-15 nipkow 2016-09-15 renamed listsum -> sum_list, listprod ~> prod_list
2016-07-14 wenzelm 2016-07-14 misc tuning and modernization;
2016-07-01 Manuel Eberl 2016-07-01 More lemmas on Gcd/Lcm
2016-05-25 wenzelm 2016-05-25 isabelle update_cartouches -c -t;
2016-04-18 haftmann 2016-04-18 capitalized GCD and LCM syntax
2016-02-26 Manuel Eberl 2016-02-26 Tuned Euclidean Rings/GCD rings
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings and tuned proofs
2016-02-17 haftmann 2016-02-17 more sophisticated GCD syntax
2016-02-17 haftmann 2016-02-17 cleansed junk-producing interpretations for gcd/lcm on nat altogether
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2016-02-17 haftmann 2016-02-17 generalized some lemmas; moved some lemmas in more appropriate places; deleted potentially dangerous simp rule
2016-02-17 haftmann 2016-02-17 more theorems concerning gcd/lcm/Gcd/Lcm
2016-02-17 haftmann 2016-02-17 further generalization and polishing
2016-02-17 haftmann 2016-02-17 pulled out legacy aliasses and infamous dvd interpretations into theory appendix
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2015-12-30 wenzelm 2015-12-30 isabelle update_cartouches -c -t;
2015-12-28 wenzelm 2015-12-28 more symbols;
2015-12-28 wenzelm 2015-12-28 prefer symbols for "abs";
2015-12-24 haftmann 2015-12-24 tuned proofs and augmented lemmas
2015-12-22 haftmann 2015-12-22 tuned proofs and augmented some lemmas
2015-12-18 Andreas Lochbihler 2015-12-18 add gcd instance for integer and serialisation to target language operations
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-11-04 ballarin 2015-11-04 Keyword 'rewrites' identifies rewrite morphisms.
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-07-08 haftmann 2015-07-08 tuned facts
2015-07-08 haftmann 2015-07-08 more cautious use of [iff] declarations
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-06-27 haftmann 2015-06-27 tuned code setup
2015-06-27 haftmann 2015-06-27 algebraic specification for set gcd
2015-06-25 wenzelm 2015-06-25 tuned proofs;
2015-06-17 wenzelm 2015-06-17 tuned proofs -- slightly faster;
2015-06-02 wenzelm 2015-06-02 tuned proof;
2015-04-30 paulson 2015-04-30 tidying some messy proofs
2015-04-08 wenzelm 2015-04-08 eliminated hard tabs;
2015-03-25 wenzelm 2015-03-25 prefer local fixes;
2015-03-10 paulson 2015-03-10 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
2015-02-15 haftmann 2015-02-15 explicit equivalence for strict order on lattices
2015-02-10 wenzelm 2015-02-10 indicate slow proof (approx. 20s);
2014-11-17 haftmann 2014-11-17 formally self-contained gcd type classes
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-30 haftmann 2014-10-30 more simp rules concerning dvd and even/odd
2014-10-26 haftmann 2014-10-26 eliminated redundancies; more simp rules