src/HOL/Library/Primes.thy
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