src/HOL/Integ/NatSimprocs.thy
2006-01-11 paulson 2006-01-11 tidied, and giving theorems names
2006-01-09 paulson 2006-01-09 tidied
2005-09-17 wenzelm 2005-09-17 tuned document;
2005-08-26 ballarin 2005-08-26 Lemmas on dvd, power and finite summation added or strengthened.
2005-08-16 paulson 2005-08-16 more simprules now have names
2005-07-12 avigad 2005-07-12 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities) added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.) renamed simplification rules for abs (abs_of_pos, etc.) renamed rules for multiplication and signs (mult_pos_pos, etc.) moved lemmas involving fractions from NatSimprocs.thy added setsum_mono3 to FiniteSet.thy added simplification rules for powers to Parity.thy
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-10-07 paulson 2004-10-07 simplification tweaks for better arithmetic reasoning
2004-10-04 paulson 2004-10-04 revised simprules for division
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-04-16 wenzelm 2004-04-16 tuned document;
2004-03-19 paulson 2004-03-19 new thms
2004-03-05 paulson 2004-03-05 some new results
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
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-04 paulson 2003-12-04 further simplifications of the integer development; converting more .ML files to Isar scripts
2003-07-24 paulson 2003-07-24 header comment
2000-11-29 paulson 2000-11-29 invoking CancelNumeralFactorFun
2000-07-25 wenzelm 2000-07-25 rearranged setup of arithmetic procedures, avoiding global reference values;
2000-05-12 paulson 2000-05-12 new dummy theory; prevents strange errors when loading NatSimprocs.ML