src/HOL/GCD.thy
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
2014-10-24 hoelzl 2014-10-24 use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
2014-10-23 haftmann 2014-10-23 downshift of theory Parity in the hierarchy
2014-10-07 wenzelm 2014-10-07 more bibtex entries; more antiquotations;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-03-19 haftmann 2014-03-19 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2013-12-26 haftmann 2013-12-26 prefer ephemeral interpretation over interpretation in proof contexts; prefer context begin ... end blocks for often-occuring assumptions; slightly more complete interpretations into abstract algebraic structures for gcd/lcm
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-15 haftmann 2013-11-15 proper code equations for Gcd and Lcm on nat and int
2013-11-05 hoelzl 2013-11-05 generalize SUP and INF to the syntactic type classes Sup and Inf
2013-07-25 haftmann 2013-07-25 factored syntactic type classes for bot and top (by Alessandro Coglio)
2013-06-19 noschinl 2013-06-19 added coprimality lemma
2013-03-26 haftmann 2013-03-26 avoid odd foundational terms after interpretation; more uniform code setup
2013-03-23 haftmann 2013-03-23 fundamental revision of big operators on sets
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-07-27 wenzelm 2012-07-27 tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
2011-12-27 haftmann 2011-12-27 prefer canonical fold on lists
2011-10-27 huffman 2011-10-27 fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
2011-10-25 huffman 2011-10-25 merge Gcd/GCD and Lcm/LCM
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-09 krauss 2011-09-09 added syntactic classes for "inf" and "sup"
2011-09-07 huffman 2011-09-07 avoid using legacy theorem names
2011-09-06 huffman 2011-09-06 avoid using legacy theorem names
2011-08-18 haftmann 2011-08-18 observe distinction between sets and predicates more properly
2011-05-20 haftmann 2011-05-20 names of fold_set locales resemble name of characteristic property more closely
2011-02-21 blanchet 2011-02-21 renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
2011-01-14 wenzelm 2011-01-14 eliminated global prems; tuned proofs;
2010-07-12 haftmann 2010-07-12 avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps