src/HOL/Integ/IntDiv.thy
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-06-16 paulson 2005-06-16 a few new integer lemmas
2005-03-23 paulson 2005-03-23 replaced bool by a new datatype "bit" for binary numerals
2004-11-24 berghofe 2004-11-24 New theorem zpower_int
2004-10-19 paulson 2004-10-19 converted some induct_tac to induct
2004-10-07 paulson 2004-10-07 simplification tweaks for better arithmetic reasoning
2004-10-01 paulson 2004-10-01 tweaking of arithmetic proofs
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-08-02 obua 2004-08-02 zdiv_int, zmod_int
2004-07-01 paulson 2004-07-01 new treatment of binary numerals
2004-06-24 paulson 2004-06-24 replaced monomorphic abs definitions by abs_if
2004-03-24 paulson 2004-03-24 streamlined treatment of quotients for the integers
2004-03-19 paulson 2004-03-19 stylistic tweaks
2004-02-15 paulson 2004-02-15 Polymorphic treatment of binary arithmetic using axclasses
2004-02-10 paulson 2004-02-10 generic of_nat and of_int functions, and generalization of iszero and neg
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-10 paulson 2003-12-10 Moving some theorems from Real/RealArith0.ML
2003-12-03 paulson 2003-12-03 Simplification of the development of Integers
2003-02-27 paulson 2003-02-27 Reorganized, moving many results about the integer dvd relation from IntPrimes to main HOL (IntDiv)
2003-01-28 nipkow 2003-01-28 pos/neg_mod_sign/bound are now simp rules.
2002-11-15 nipkow 2002-11-15 added zdvd_iff_zmod_eq_0
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-07-01 nipkow 2002-07-01 modified Larry's changes to make div/mod a numeral work in arith.
2002-06-29 paulson 2002-06-29 new splitting rules for zdiv, zmod
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-06 wenzelm 2001-10-06 * sane numerals (stage 2): plain "num" syntax (removed "#");
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;
2000-05-21 wenzelm 2000-05-21 replaced {{ }} by { };
1999-10-04 wenzelm 1999-10-04 IntArith;
1999-07-13 paulson 1999-07-13 change to force (m div 0 = 0)
1999-07-08 paulson 1999-07-08 Introduction of integer division algorithm Renaming of theorems from _nat0 to _int0 and _nat1 to _int1