src/HOL/Real/RComplete.thy
2008-09-02 nipkow 2008-09-02 Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and distributed them over Real/ (to do with bijections and density). Library/NatPair became Nat_Int_Bij and made that part of Main.
2008-07-02 haftmann 2008-07-02 cleaned up some code generator configuration
2007-10-23 nipkow 2007-10-23 went back to >0
2007-10-21 nipkow 2007-10-21 More changes from >0 to ~=0::nat
2007-08-20 huffman 2007-08-20 remove int_of_nat
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
2007-06-11 huffman 2007-06-11 remove references to constant int::nat=>int
2007-05-19 huffman 2007-05-19 remove dependence on Hilbert_Choice.thy
2007-05-18 huffman 2007-05-18 avoid using real_mult_inverse_left; cleaned up
2007-05-17 huffman 2007-05-17 avoid using redundant lemmas from RealDef.thy
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
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