src/HOL/Real/rat_arith.ML
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-16 wenzelm 2008-06-16 eliminated OldGoals.inst;
2008-06-11 wenzelm 2008-06-11 OldGoals.inst;
2007-08-09 haftmann 2007-08-09 localized of_nat
2007-07-31 wenzelm 2007-07-31 tuned LinArith setup;
2007-06-12 huffman 2007-06-12 thm antiquotations
2007-05-23 huffman 2007-05-23 remove unused simproc definition
2007-05-23 huffman 2007-05-23 remove redundant simproc
2007-04-26 haftmann 2007-04-26 slightly tuned
2007-03-29 haftmann 2007-03-29 dropped legacy ML bindings
2006-11-08 wenzelm 2006-11-08 removed theory NatArith (now part of Nat);
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-05-04 nipkow 2005-05-04 fixed lin.arith
2004-09-07 nipkow 2004-09-07 fixed discrete field.
2004-09-06 nipkow 2004-09-06 made mult_mono_thms generic.
2004-08-06 nipkow 2004-08-06 Initial changes to extend arithmetic from individual types to type classes.
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-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-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