src/HOL/Real/real_arith.ML
2006-01-19 ago setup: theory -> theory;
2005-10-17 ago change_claset/simpset;
2005-07-14 ago accomodate change of real_of_XXX;
2005-05-04 ago fixed lin.arith
2005-04-07 ago reverted renaming of Some/None in comments and strings;
2005-02-13 ago Deleted Library.option type.
2004-09-07 ago fixed discrete field.
2004-09-06 ago made mult_mono_thms generic.
2004-06-24 ago replaced monomorphic abs definitions by abs_if
2004-03-30 ago tidied
2004-03-25 ago new treatment of equivalence classes
2004-03-19 ago removed redundant thms
2004-03-02 ago fixed bugs in the setup of arithmetic procedures
2004-02-17 ago further tweaks to the numeric theories
2004-02-15 ago Polymorphic treatment of binary arithmetic using axclasses
2004-01-28 ago tidying up arithmetic for the hyperreals
2004-01-28 ago converted Real/Lubs to Isar script. Converting arithmetic setup
2004-01-27 ago replacing HOL/Real/PRat, PNat by the rational number development
2004-01-14 ago fixed old bugs in "decomp" (conversion from term to lin.arith. format).
2004-01-14 ago Told linear arithmetic package about injections "real" from nat/int into real.
2004-01-12 ago Modified real arithmetic simplification
2004-01-03 ago Deleting more redundant theorems
2004-01-01 ago tweaking of lemmas in RealDef, RealOrd
2003-12-23 ago new theorems
2003-12-23 ago more ML bindings
2003-12-22 ago new binding
2003-12-22 ago removing obsolete bindings
2003-12-19 ago tidying first part of HyperArith0.ML, using generic lemmas
2003-12-12 ago moving some division theorems to Ring_and_Field
2003-12-10 ago combining Real/{RealArith0,real_arith}.ML
2003-12-10 ago Moving some theorems from Real/RealArith0.ML
2001-01-01 ago minor tidying of simprocs
2000-12-21 ago rational linear arithmetic
2000-12-18 ago moved mk_bin from Numerals to HOLogic
2000-12-01 ago Linear arithmetic now copes with mixed nat/int formulae.
2000-07-25 ago rearranged setup of arithmetic procedures, avoiding global reference values;