src/HOL/Real/RComplete.thy
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-06-11 wenzelm 2006-06-11 fixed subst step;
2006-06-02 wenzelm 2006-06-02 misc cleanup;
2005-07-19 wenzelm 2005-07-19 some structured proofs on completeness;
2005-07-14 wenzelm 2005-07-14 accomodate change of real_of_XXX;
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