src/HOL/NumberTheory/IntPrimes.thy
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
2003-12-03 paulson 2003-12-03 Simplification of the development of Integers
2003-08-29 ballarin 2003-08-29 Methods rule_tac etc support static (Isar) contexts.
2003-02-27 paulson 2003-02-27 Reorganized, moving many results about the integer dvd relation from IntPrimes to main HOL (IntDiv)
2003-02-26 paulson 2003-02-26 zprime_def fixes by Jeremy Avigad
2003-01-28 nipkow 2003-01-28 pos/neg_mod_sign/bound are now simp rules.
2002-10-08 nipkow 2002-10-08 Got rid of rotates because of new simplifier
2002-09-30 berghofe 2002-09-30 Adapted to new simplifier.
2002-08-27 wenzelm 2002-08-27 *** empty log message ***
2002-08-23 nipkow 2002-08-23 Added div+mod cancelling simproc
2002-05-31 paulson 2002-05-31 finished an incomplete proof
2002-05-30 nipkow 2002-05-30 Modifications due to enhanced linear arithmetic.
2002-05-28 paulson 2002-05-28 conversion of IntDiv.thy to Isar format
2001-10-22 paulson 2001-10-22 Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.
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-02-04 wenzelm 2001-02-04 HOL-NumberTheory: converted to new-style format and proper document setup;
2000-10-03 wenzelm 2000-10-03 tuned deps;
2000-09-13 paulson 2000-09-13 zgcd now works for negative integers
2000-08-03 paulson 2000-08-03 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen