src/HOL/Real/RComplete.thy
2005-07-13 avigad 2005-07-13 fixed typos in theorem names
2005-07-13 avigad 2005-07-13 Additions to the Real (and Hyperreal) libraries: RealDef.thy: lemmas relating nats, ints, and reals reversed direction of real_of_int_mult, etc. (now they agree with nat versions) SEQ.thy and Series.thy: various additions RComplete.thy: lemmas involving floor and ceiling introduced natfloor and natceiling Log.thy: various additions
2005-02-21 nipkow 2005-02-21 comprehensive cleanup, replacing sumr by setsum
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-04-22 paulson 2004-04-22 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate places
2004-03-19 paulson 2004-03-19 removed redundant thms
2004-02-15 paulson 2004-02-15 Polymorphic treatment of binary arithmetic using axclasses
2004-01-27 paulson 2004-01-27 replacing HOL/Real/PRat, PNat by the rational number development of Markus Wenzel
2000-07-24 wenzelm 2000-07-24 changed deps;
1999-08-19 paulson 1999-08-19 real literals using binary arithmetic
1999-08-16 paulson 1999-08-16 inserted Id: lines
1998-06-25 paulson 1998-06-25 Installation of target HOL-Real