src/HOL/GCD.thy
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
2009-02-21 nipkow 2009-02-21 Removed subsumed lemmas
2009-01-31 nipkow 2009-01-31 added some simp rules
2009-01-28 haftmann 2009-01-28 Plain, Main form meeting points in import hierarchy
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s
2005-07-08 nipkow 2005-07-08 Used to be in Library/Primes