src/HOL/Library/Primes.thy
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-22 nipkow 2009-02-22 added lemmas
2009-02-21 nipkow 2009-02-21 Removed subsumed lemmas
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-07-21 chaieb 2008-07-21 Theorems divides_le, ind_euclid, bezout_lemma, bezout_add, bezout, bezout_add_strong, gcd_unique,gcd_eq, bezout_gcd, bezout_gcd_strong, gcd_mult_distrib, gcd_bezout to GCD.thy
2008-07-18 haftmann 2008-07-18 moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-07-14 chaieb 2008-07-14 Fixed proofs.
2008-07-14 haftmann 2008-07-14 unified curried gcd, lcm, zgcd, zlcm
2008-07-07 haftmann 2008-07-07 absolute imports of HOL/*.thy theories
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-06-10 haftmann 2008-06-10 removed some dubious code lemmas
2008-04-28 haftmann 2008-04-28 thms Max_ge, Min_le: dropped superfluous premise
2008-02-27 chaieb 2008-02-27 Removed theorems from default simpset
2008-02-26 wenzelm 2008-02-26 tuned document;
2008-02-25 chaieb 2008-02-25 More primality theorems
2007-12-10 haftmann 2007-12-10 explicit import of theory ATP_Linkup
2007-07-18 paulson 2007-07-18 tidying using metis
2007-04-13 wenzelm 2007-04-13 tuned document (headers, sections, spacing);
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-08 wenzelm 2006-11-08 moved theories Parity, GCD, Binomial to Library;
2006-02-16 wenzelm 2006-02-16 new-style definitions/abbreviations;
2005-07-08 nipkow 2005-07-08 moved gcd to new GCD.thy
2005-07-01 nipkow 2005-07-01 prime is a predicate now.
2005-03-25 paulson 2005-03-25 tidied up
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-05-06 wenzelm 2004-05-06 tuned document;
2004-01-12 paulson 2004-01-12 Added lemmas to Ring_and_Field with slightly modified simplification rules Deleted some little-used integer theorems, replacing them by the generic ones in Ring_and_Field Consolidated integer powers
2002-05-30 nipkow 2002-05-30 Modifications due to enhanced linear arithmetic.
2002-03-06 wenzelm 2002-03-06 added two_is_prime;
2002-01-13 wenzelm 2002-01-13 prime_dvd_power_two;
2001-11-26 wenzelm 2001-11-26 gcd_dvd1 and gcd_dvd2 proven simultaneously;
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-08-06 nipkow 2001-08-06 turned translation for 1::nat into def. introduced 1' and replaced most occurrences of 1 by 1'.
2001-06-13 paulson 2001-06-13 New proof of gcd_zero after a change to Divides.ML made the old one fail
2001-06-09 wenzelm 2001-06-09 tuned
2001-06-09 wenzelm 2001-06-09 tuned Primes theory;
2001-06-09 paulson 2001-06-09 moved Primes.thy from NumberTheory to Library