src/HOL/GCD.thy
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
2010-01-01 nipkow 2010-01-01 removed FIXME
2009-12-08 haftmann 2009-12-08 resorted code equations from "old" number theory version
2009-12-04 nipkow 2009-12-04 removed redundant lemma
2009-11-13 nipkow 2009-11-13 renamed lemmas "anti_sym" -> "antisym"
2009-10-29 haftmann 2009-10-29 moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
2009-10-23 blanchet 2009-10-23 continuation of Nitpick's integration into Isabelle; added examples, and integrated non-Main theories better.
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-10-06 haftmann 2009-10-06 added syntactic Inf and Sup
2009-09-01 haftmann 2009-09-01 some reorganization of number theory
2009-08-26 nipkow 2009-08-26 got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class.
2009-07-21 nipkow 2009-07-21 Made dvd/gcd/lcm a complete lattice by introducing Gcd/GCD/Lcm/LCM
2009-07-21 nipkow 2009-07-21 Tests for executability of "prime"
2009-07-17 berghofe 2009-07-17 merged
2009-07-14 berghofe 2009-07-14 merged
2009-07-10 avigad 2009-07-10 Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
2009-07-15 nipkow 2009-07-15 Made "prime" executable
2009-07-13 berghofe 2009-07-13 Tuned proof of lcm_1_iff_int, because metis produced enormous proof term.
2009-07-12 nipkow 2009-07-12 more gcd/lcm lemmas
2009-07-12 nipkow 2009-07-12 More about gcd/lcm, and some cleaning up
2009-07-07 nipkow 2009-07-07 renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
2009-06-26 nipkow 2009-06-26 lcm abs lemmas
2009-06-26 nipkow 2009-06-26 gcd abs lemmas
2009-06-25 nipkow 2009-06-25 Cleaned up GCD
2009-06-23 nipkow 2009-06-23 new lemmas
2009-06-21 nipkow 2009-06-21 new lemmas
2009-06-20 nipkow 2009-06-20 added lemmas; tuned
2009-06-20 nipkow 2009-06-20 new lemmas and tuning
2009-06-18 huffman 2009-06-18 more [code del] declarations
2009-06-17 huffman 2009-06-17 new GCD library, courtesy of Jeremy Avigad
2009-03-27 haftmann 2009-03-27 normalized imports
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-24 huffman 2009-02-24 make more proofs work whether or not One_nat_def is a simp rule