src/HOL/Real/PReal.thy
2008-08-11 haftmann 2008-08-11 re-arranged class dense_linear_order
2008-07-25 haftmann 2008-07-25 added class preorder
2008-06-10 haftmann 2008-06-10 removed some dubious code lemmas
2008-05-07 berghofe 2008-05-07 Adapted to encoding of sets as predicates
2008-04-07 haftmann 2008-04-07 explicit definition for "/"
2008-04-02 haftmann 2008-04-02 explicit instantiation
2007-12-07 haftmann 2007-12-07 instantiation target rather than legacy instance
2007-11-29 haftmann 2007-11-29 instance command as rudimentary class target
2007-08-24 haftmann 2007-08-24 moved class dense_linear_order to Orderings.thy
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
2007-06-07 huffman 2007-06-07 define (1::preal); clean up instance declarations
2007-06-07 huffman 2007-06-07 instance preal :: ordered_cancel_ab_semigroup_add
2007-04-15 wenzelm 2007-04-15 read prop as prop, not term;
2007-03-20 haftmann 2007-03-20 added instance for lattice
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-09-09 huffman 2006-09-09 cleaned up
2006-06-02 wenzelm 2006-06-02 misc cleanup;
2005-12-19 nipkow 2005-12-19 fixed proof
2005-12-17 wenzelm 2005-12-17 simp del: empty_Collect_eq;
2005-11-21 paulson 2005-11-21 tweak
2005-09-15 huffman 2005-09-15 add header
2005-07-12 avigad 2005-07-12 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities) added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.) renamed simplification rules for abs (abs_of_pos, etc.) renamed rules for multiplication and signs (mult_pos_pos, etc.) moved lemmas involving fractions from NatSimprocs.thy added setsum_mono3 to FiniteSet.thy added simplification rules for powers to Parity.thy
2004-12-15 paulson 2004-12-15 removal of archaic Abs/Rep proofs
2004-10-07 paulson 2004-10-07 simplification tweaks for better arithmetic reasoning
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