src/HOL/Integ/IntArith.thy
2004-08-16 nipkow 2004-08-16 New theory header syntax.
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-05-11 obua 2004-05-11 changes made due to new Ring_and_Field theory
2004-03-24 paulson 2004-03-24 streamlined treatment of quotients for the integers
2004-03-19 paulson 2004-03-19 stylistic tweaks
2004-03-05 paulson 2004-03-05 some new results
2004-02-17 paulson 2004-02-17 further tweaks to the numeric theories
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-27 paulson 2004-01-27 replacing HOL/Real/PRat, PNat by the rational number development of Markus Wenzel
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-15 paulson 2003-12-15 more general lemmas for Ring_and_Field
2003-12-04 paulson 2003-12-04 Tidying of the integer development; towards removing the abel_cancel simproc
2003-12-03 paulson 2003-12-03 Simplification of the development of Integers
2003-11-24 paulson 2003-11-24 conversion of integers to use Ring_and_Field; new lemmas for Ring_and_Field
2003-11-18 paulson 2003-11-18 conversion of ML to Isar scripts
2003-03-06 paulson 2003-03-06 new simprule for int (nat n) and consequential changes
2003-02-27 paulson 2003-02-27 Reorganized, moving many results about the integer dvd relation from IntPrimes to main HOL (IntDiv)
2002-10-29 nipkow 2002-10-29 added induction thms
2002-09-25 nipkow 2002-09-25 added nat_split
2001-11-03 wenzelm 2001-11-03 tuned;
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.
2000-12-01 nipkow 2000-12-01 Linear arithmetic now copes with mixed nat/int formulae.
2000-07-25 wenzelm 2000-07-25 rearranged setup of arithmetic procedures, avoiding global reference values;
2000-07-01 nipkow 2000-07-01 Defined abs on int.
1999-10-04 wenzelm 1999-10-04 simprocs now in IntArith;