src/HOL/Real/PReal.thy
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-07-16 nipkow 2004-07-16 Corrected TeX problem.
2004-07-01 paulson 2004-07-01 new treatment of binary numerals
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-13 kleing 2004-04-13 hence -> from calculation have
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
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-02-05 paulson 2004-02-05 tidying up, especially the Complex numbers
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-01 paulson 2004-01-01 conversion of Real/PReal to Isar script; type "complex" is now in class "field"
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.
1999-10-11 paulson 1999-10-11 replaced {x. True} by UNIV to work with the new simprule, Collect_const
1999-08-16 paulson 1999-08-16 inserted Id: lines
1999-07-23 paulson 1999-07-23 heavily revised by Jacques: coercions have alphabetic names; exponentiation is available, etc.
1998-06-25 paulson 1998-06-25 Installation of target HOL-Real