src/HOL/Integ/NatBin.thy
2005-06-16 paulson 2005-06-16 a few new integer lemmas
2005-05-16 paulson 2005-05-16 Use of IntInf.int instead of int in most numeric simprocs; avoids integer overflow in SML/NJ
2005-05-04 nipkow 2005-05-04 Fixing a problem with lin.arith.
2005-03-23 paulson 2005-03-23 replaced bool by a new datatype "bit" for binary numerals
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-17 nipkow 2005-01-17 Removed div/mod ML code because it fails for 0.
2005-01-14 nipkow 2005-01-14 made diff_less a simp rule
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-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-08-16 berghofe 2004-08-16 Replaced `div and `mod in consts_code section by div and mod.
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-15 paulson 2004-03-15 new lemma
2004-03-08 paulson 2004-03-08 generic theorems about exponentials; general tidying up
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
2004-02-29 berghofe 2004-02-29 Added specific code generator for number_of.
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-10 paulson 2003-12-10 Moving some theorems from Real/RealArith0.ML
2003-12-04 paulson 2003-12-04 further simplifications of the integer development; converting more .ML files to Isar scripts
2003-12-04 paulson 2003-12-04 Tidying of the integer development; towards removing the abel_cancel simproc
2003-09-22 berghofe 2003-09-22 Improved efficiency of code generated for functions int and nat.
2002-08-12 nipkow 2002-08-12 *** empty log message ***
2002-05-31 nipkow 2002-05-31 Now arith can deal with div/mod arbitrary nat numerals.
2002-05-15 nipkow 2002-05-15 Set up arith to deal with div 2 and mod 2.
2002-03-07 wenzelm 2002-03-07 renamed nat_number_of to nat_number (avoid clash with separate theorem);
2002-02-25 berghofe 2002-02-25 Introduced variants of operators + * ~ constrained to type int (to make SML/NJ happy).
2002-01-23 wenzelm 2002-01-23 tuned; lemmas nat_number_of;
2001-12-10 berghofe 2001-12-10 Added code generator setup.
2001-08-07 paulson 2001-08-07 Tweaks for 1 -> 1'
2001-08-06 nipkow 2001-08-06 turned translation for 1::nat into def. introduced 1' and replaced most occurrences of 1 by 1'.
2000-12-01 nipkow 2000-12-01 Linear arithmetic now copes with mixed nat/int formulae.
2000-08-03 paulson 2000-08-03 introduction of integer exponentiation
1999-07-19 paulson 1999-07-19 NatBin: binary arithmetic for the naturals