src/HOL/Real/RealArith.thy
2004-02-10 paulson 2004-02-10 generic of_nat and of_int functions, and generalization of iszero and neg
2004-01-28 paulson 2004-01-28 tidying up arithmetic for the hyperreals
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 Modified real arithmetic simplification
2004-01-01 paulson 2004-01-01 tweaking of lemmas in RealDef, RealOrd
2003-12-25 paulson 2003-12-25 re-organized some hyperreal and real lemmas
2003-12-23 paulson 2003-12-23 new theorems
2003-12-22 paulson 2003-12-22 removing obsolete bindings
2003-12-15 paulson 2003-12-15 more general lemmas for Ring_and_Field
2003-12-13 paulson 2003-12-13 absolute value theorems moved to HOL/Ring_and_Field
2003-12-12 paulson 2003-12-12 moving some division theorems to Ring_and_Field
2003-12-11 paulson 2003-12-11 removal of abel_cancel from Real
2003-12-10 paulson 2003-12-10 Moving some theorems from Real/RealArith0.ML
2003-12-05 paulson 2003-12-05 Converting more of the "real" development to Isar scripts
2003-12-02 paulson 2003-12-02 More re-organising of numerical theorems
2003-11-28 paulson 2003-11-28 conversion of some Real theories to Isar scripts
2000-12-21 nipkow 2000-12-21 rational linear arithmetic
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;