src/HOL/Real/real_arith.ML
2007-07-31 wenzelm 2007-07-31 tuned LinArith setup;
2007-05-23 huffman 2007-05-23 remove unused simproc definition
2007-05-23 huffman 2007-05-23 remove redundant simproc; remove legacy ML bindings
2007-05-14 huffman 2007-05-14 move lemmas to RealPow.thy; tuned proofs
2007-05-14 huffman 2007-05-14 remove redundant lemmas
2006-07-29 webertj 2006-07-29 lin_arith_prover splits certain operators (e.g. min, max, abs)
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-10-17 wenzelm 2005-10-17 change_claset/simpset;
2005-07-14 wenzelm 2005-07-14 accomodate change of real_of_XXX;
2005-05-04 nipkow 2005-05-04 fixed lin.arith
2005-04-07 wenzelm 2005-04-07 reverted renaming of Some/None in comments and strings;
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-09-07 nipkow 2004-09-07 fixed discrete field.
2004-09-06 nipkow 2004-09-06 made mult_mono_thms generic.
2004-06-24 paulson 2004-06-24 replaced monomorphic abs definitions by abs_if
2004-03-30 paulson 2004-03-30 tidied
2004-03-25 paulson 2004-03-25 new treatment of equivalence classes
2004-03-19 paulson 2004-03-19 removed redundant thms
2004-03-02 paulson 2004-03-02 fixed bugs in the setup of arithmetic procedures
2004-02-17 paulson 2004-02-17 further tweaks to the numeric theories
2004-02-15 paulson 2004-02-15 Polymorphic treatment of binary arithmetic using axclasses
2004-01-28 paulson 2004-01-28 tidying up arithmetic for the hyperreals
2004-01-28 paulson 2004-01-28 converted Real/Lubs to Isar script. Converting arithmetic setup files to be polymorphic.
2004-01-27 paulson 2004-01-27 replacing HOL/Real/PRat, PNat by the rational number development of Markus Wenzel
2004-01-14 nipkow 2004-01-14 fixed old bugs in "decomp" (conversion from term to lin.arith. format). updated instantiation of real lin.arith.
2004-01-14 nipkow 2004-01-14 Told linear arithmetic package about injections "real" from nat/int into real.
2004-01-12 paulson 2004-01-12 Modified real arithmetic simplification
2004-01-03 paulson 2004-01-03 Deleting more redundant theorems
2004-01-01 paulson 2004-01-01 tweaking of lemmas in RealDef, RealOrd
2003-12-23 paulson 2003-12-23 new theorems
2003-12-23 paulson 2003-12-23 more ML bindings
2003-12-22 paulson 2003-12-22 new binding
2003-12-22 paulson 2003-12-22 removing obsolete bindings
2003-12-19 paulson 2003-12-19 tidying first part of HyperArith0.ML, using generic lemmas
2003-12-12 paulson 2003-12-12 moving some division theorems to Ring_and_Field
2003-12-10 paulson 2003-12-10 combining Real/{RealArith0,real_arith}.ML
2003-12-10 paulson 2003-12-10 Moving some theorems from Real/RealArith0.ML
2001-01-01 paulson 2001-01-01 minor tidying of simprocs
2000-12-21 nipkow 2000-12-21 rational linear arithmetic
2000-12-18 nipkow 2000-12-18 moved mk_bin from Numerals to HOLogic first steps towards rational lin arith
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;