src/HOL/Integ/NatBin.thy
2006-01-19 ago setup: theory -> theory;
2006-01-17 ago substantial improvements in code generator
2005-09-29 ago simprules need names
2005-09-27 ago nat_number_of is no longer declared as code lemma, since this turned
2005-09-21 ago Declared nat_number_of as code lemma.
2005-08-16 ago more simprules now have names
2005-07-12 ago added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
2005-07-01 ago Moved code generator setup from NatBin to IntDef.
2005-06-16 ago a few new integer lemmas
2005-05-16 ago Use of IntInf.int instead of int in most numeric simprocs; avoids
2005-05-04 ago Fixing a problem with lin.arith.
2005-03-23 ago replaced bool by a new datatype "bit" for binary numerals
2005-02-13 ago Deleted Library.option type.
2005-01-17 ago Removed div/mod ML code because it fails for 0.
2005-01-14 ago made diff_less a simp rule
2004-10-19 ago converted some induct_tac to induct
2004-10-07 ago simplification tweaks for better arithmetic reasoning
2004-08-18 ago import -> imports
2004-08-16 ago New theory header syntax.
2004-08-16 ago Replaced `div and `mod in consts_code section by div and mod.
2004-07-01 ago new treatment of binary numerals
2004-06-24 ago replaced monomorphic abs definitions by abs_if
2004-05-11 ago changes made due to new Ring_and_Field theory
2004-03-15 ago new lemma
2004-03-08 ago generic theorems about exponentials; general tidying up
2004-03-04 ago new material from Avigad, and simplified treatment of division by 0
2004-02-29 ago Added specific code generator for number_of.
2004-02-17 ago further tweaks to the numeric theories
2004-02-15 ago Polymorphic treatment of binary arithmetic using axclasses
2004-02-10 ago generic of_nat and of_int functions, and generalization of iszero
2004-01-27 ago replacing HOL/Real/PRat, PNat by the rational number development
2004-01-12 ago Added lemmas to Ring_and_Field with slightly modified simplification rules
2003-12-10 ago Moving some theorems from Real/RealArith0.ML
2003-12-04 ago further simplifications of the integer development; converting more .ML files
2003-12-04 ago Tidying of the integer development; towards removing the
2003-09-22 ago Improved efficiency of code generated for functions int and nat.
2002-08-12 ago *** empty log message ***
2002-05-31 ago Now arith can deal with div/mod arbitrary nat numerals.
2002-05-15 ago Set up arith to deal with div 2 and mod 2.
2002-03-07 ago renamed nat_number_of to nat_number (avoid clash with separate theorem);
2002-02-25 ago Introduced variants of operators + * ~ constrained to type int
2002-01-23 ago tuned;
2001-12-10 ago Added code generator setup.
2001-08-07 ago Tweaks for 1 -> 1'
2001-08-06 ago turned translation for 1::nat into def.
2000-12-01 ago Linear arithmetic now copes with mixed nat/int formulae.
2000-08-03 ago introduction of integer exponentiation
1999-07-19 ago NatBin: binary arithmetic for the naturals