src/HOL/Import/HOL/arithmetic.imp
2009-06-24 nipkow 2009-06-24 corrected and unified thm names
2009-04-15 haftmann 2009-04-15 theory NatBin now named Nat_Numeral
2008-01-21 haftmann 2008-01-21 adjusted to constant and theorem renames
2007-10-12 haftmann 2007-10-12 moved class power to theory Power
2007-07-20 haftmann 2007-07-20 moved class ord from Orderings.thy to HOL.thy
2007-05-30 haftmann 2007-05-30 updated
2007-05-17 haftmann 2007-05-17 canonical prefixing of class constants
2006-11-18 haftmann 2006-11-18 dvd_def now with object equality
2006-11-08 wenzelm 2006-11-08 removed theory NatArith (now part of Nat);
2006-03-17 haftmann 2006-03-17 renamed op < <= to Orderings.less(_eq)
2006-03-10 haftmann 2006-03-10 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
2005-09-29 wenzelm 2005-09-29 updated;
2005-08-29 obua 2005-08-29 Updated import.
2005-07-13 paulson 2005-07-13 generlization of some "nat" theorems
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-04-01 skalberg 2005-04-01 Updated import configuration.
2004-05-21 wenzelm 2004-05-21 updated;
2004-04-02 skalberg 2004-04-02 Added HOL proof importer.