src/HOL/Real/RealDef.thy
2004-07-26 paulson 2004-07-26 converting Hyperreal/Transcendental to Isar script
2004-07-01 paulson 2004-07-01 new treatment of binary numerals
2004-06-24 paulson 2004-06-24 replaced monomorphic abs definitions by abs_if
2004-05-18 obua 2004-05-18 Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
2004-05-11 obua 2004-05-11 changes made due to new Ring_and_Field theory
2004-05-01 wenzelm 2004-05-01 tuned instance statements;
2004-04-23 paulson 2004-04-23 congruent2 now allows different equiv relations
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-08 paulson 2004-03-08 generic theorems about exponentials; general tidying up
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
2004-03-02 paulson 2004-03-02 fixed bugs in the setup of arithmetic procedures
2004-03-01 paulson 2004-03-01 new Ring_and_Field hierarchy, eliminating redundant axioms
2004-02-19 ballarin 2004-02-19 Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.
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-27 paulson 2004-01-27 replacing HOL/Real/PRat, PNat by the rational number development of Markus Wenzel
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 conversion of Real/PReal to Isar script; type "complex" is now in class "field"
2004-01-01 paulson 2004-01-01 tweaking of lemmas in RealDef, RealOrd
2003-12-25 paulson 2003-12-25 re-organized some hyperreal and real lemmas
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
2002-08-08 wenzelm 2002-08-08 tuned;
2001-11-09 wenzelm 2001-11-09 eliminated old "symbols" syntax, use "xsymbols" instead;
2001-11-02 paulson 2001-11-02 Numerals and simprocs for types real and hypreal. The abstract constants 0, 1 and binary numerals work harmoniously.
2001-10-08 wenzelm 2001-10-08 sane numerals (stage 3): provide generic "1" on all number types;
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-01-16 paulson 2001-01-16 renamings: real_of_nat, real_of_int -> (overloaded) real inf_close -> approx SReal -> Reals SNat -> Nats
2001-01-09 nipkow 2001-01-09 *** empty log message ***
2001-01-05 nipkow 2001-01-05 ^^ -> ``` Univalent -> single_valued
2001-01-04 paulson 2001-01-04 more tidying, especially to remove real_of_posnat
2000-12-30 paulson 2000-12-30 tidying, and separation of HOL-Hyperreal from HOL-Real
2000-12-12 paulson 2000-12-12 first stage in tidying up Real and Hyperreal. Factor cancellation simprocs inverse #0 = #0 simprules for division corrected ambigous syntax definitions in Hyperreal
2000-12-06 bauerg 2000-12-06 converted rinv to inverse;
2000-07-19 paulson 2000-07-19 changed / to // for quotienting; general tidying
2000-07-16 wenzelm 2000-07-16 use split syntax;
2000-06-07 paulson 2000-06-07 First round of changes, towards installation of simprocs * replacing 0r by (0::real0 * better rewriting, especially pulling out signs in (-x)*y = - (x*y), etc.
1999-08-16 paulson 1999-08-16 inserted Id: lines
1999-07-29 paulson 1999-07-29 added parentheses to cope with a possible reduction of the precedence of unary minus
1999-07-23 paulson 1999-07-23 heavily revised by Jacques: coercions have alphabetic names; exponentiation is available, etc.
1998-11-02 paulson 1998-11-02 increased precedence of unary minus from 80 to 100 requires a similar increase for %# and %%#
1998-10-01 paulson 1998-10-01 Revised version with Abelian group simprocs