src/HOL/GCD.thy
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
2010-03-11 haftmann 2010-03-11 tuned prefixes of ac interpretations
2010-03-08 haftmann 2010-03-08 transfer: avoid camel case
2010-02-24 haftmann 2010-02-24 crossproduct coprimality lemmas
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-01-28 haftmann 2010-01-28 dropped mk_left_commute; use interpretation of locale abel_semigroup instead
2010-01-10 berghofe 2010-01-10 Adapted to changes in induct method.
2010-01-01 nipkow 2010-01-01 added lemmas
2010-01-01 nipkow 2010-01-01 added lemma