src/HOL/Hyperreal/hypreal_arith.ML
2007-07-31 wenzelm 2007-07-31 tuned LinArith setup;
2007-07-31 wenzelm 2007-07-31 arith method setup: proper context;
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-09-16 huffman 2005-09-16 fix names in hypreal_arith.ML
2005-09-09 huffman 2005-09-09 starfun, starset, and other functions on NS types are now polymorphic; many similar theorems have been generalized and merged; (star_n X) replaces (Abs_star(starrel `` {X})); many proofs have been simplified with the transfer tactic.
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-02-15 paulson 2004-02-15 Polymorphic treatment of binary arithmetic using axclasses
2004-01-29 paulson 2004-01-29 simplifications in the hyperreals
2004-01-28 paulson 2004-01-28 tidying up arithmetic for the hyperreals
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-27 paulson 2003-12-27 re-organized numeric lemmas
2003-12-22 paulson 2003-12-22 moving HyperArith0.ML to other theories
2003-12-19 paulson 2003-12-19 tidying first part of HyperArith0.ML, using generic lemmas
2000-12-30 paulson 2000-12-30 separation of HOL-Hyperreal from HOL-Real