2004-01-09 paulson 2004-01-09 Defining the type class "ringpower" and deleting superseded theorems for types nat, int, real, hypreal
2004-01-06 paulson 2004-01-06 Ring_and_Field now requires axiom add_left_imp_eq for semirings. This allows more theorems to be proved for semirings, but requires a redundant axiom to be proved for rings, etc.
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-23 paulson 2003-12-23 new theorems
2003-12-19 paulson 2003-12-19 tidying first part of HyperArith0.ML, using generic lemmas
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-10 paulson 2003-12-10 Moving some theorems from Real/RealArith0.ML
2003-12-07 paulson 2003-12-07 re-organisation of Real/RealArith0.ML; more `Isar scripts
2003-12-05 paulson 2003-12-05 more field division lemmas transferred from Real to Ring_and_Field
2003-12-04 paulson 2003-12-04 Tidying of the integer development; towards removing the abel_cancel simproc
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
2003-11-27 paulson 2003-11-27 Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files. New theorems for Ring_and_Field. Fixing affected proofs.
2003-11-25 paulson 2003-11-25 More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas to Isar script.
2003-11-24 paulson 2003-11-24 conversion of integers to use Ring_and_Field; new lemmas for Ring_and_Field
2003-11-21 paulson 2003-11-21 HOL: installation of Ring_and_Field as the basis for Naturals and Reals