src/HOL/Real/RealDef.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-08-26 nipkow 2008-08-26 Defined rationals (Rats) globally in Rational. Chractarized them with a few lemmas in RealDef, one of them from Sqrt.
2008-08-23 nipkow 2008-08-23 added const Rational added more function puzzles
2008-08-11 haftmann 2008-08-11 rudimentary code setup for set operations
2008-07-25 haftmann 2008-07-25 added class preorder
2008-07-21 chaieb 2008-07-21 Tuned and simplified proofs
2008-07-18 haftmann 2008-07-18 refined code generator setup for rational numbers; more simplification rules for rational numbers
2008-07-11 haftmann 2008-07-11 improved code generator setup
2008-06-10 haftmann 2008-06-10 removed some dubious code lemmas
2008-04-22 haftmann 2008-04-22 constant HOL.eq now qualified
2008-04-02 haftmann 2008-04-02 explicit class "eq" for operational equality
2008-01-25 haftmann 2008-01-25 improved code theorem setup
2008-01-10 berghofe 2008-01-10 New interface for test data generators.
2008-01-02 haftmann 2008-01-02 splitted class uminus from class minus
2007-12-07 haftmann 2007-12-07 instantiation target rather than legacy instance
2007-12-05 obua 2007-12-05 instance int,real :: lordered_ring
2007-11-29 haftmann 2007-11-29 instance command as rudimentary class target
2007-11-06 haftmann 2007-11-06 renamed lordered_*_* to lordered_*_add_*; further localization
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-10-21 nipkow 2007-10-21 Eliminated most of the neq0_conv occurrences. As a result, many theorems had to be rephrased with ~= 0 instead of > 0.
2007-10-20 chaieb 2007-10-20 fixed proofs
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated IntInf.int, integer);
2007-09-18 haftmann 2007-09-18 renamed constructor RealC to Ratreal
2007-09-06 berghofe 2007-09-06 New code generator setup (taken from Library/Executable_Real.thy, also works for old code generator).
2007-09-01 nipkow 2007-09-01 final(?) iteration of sgn saga.
2007-08-09 haftmann 2007-08-09 adaptions for code generation
2007-07-31 wenzelm 2007-07-31 arith method setup: proper context;
2007-07-20 haftmann 2007-07-20 split class abs from class minus
2007-06-24 nipkow 2007-06-24 tuned and used field_simps
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-06-20 huffman 2007-06-20 remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
2007-06-20 huffman 2007-06-20 change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
2007-06-07 huffman 2007-06-07 remove redundant lemmas
2007-06-07 huffman 2007-06-07 remove references to preal-specific theorems
2007-06-07 huffman 2007-06-07 define (1::preal); clean up instance declarations
2007-05-19 nipkow 2007-05-19 added code generation based on Isabelle's rat type.
2007-05-14 huffman 2007-05-14 move lemmas to RealPow.thy; tuned proofs
2007-05-14 huffman 2007-05-14 remove redundant lemmas
2007-05-14 huffman 2007-05-14 cleaned up
2007-03-16 haftmann 2007-03-16 added lattice definitions
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-09-16 huffman 2006-09-16 define new constant of_real for class real_algebra_1; define set Reals as range of_real; add lemmas about of_real and Reals
2006-09-06 haftmann 2006-09-06 got rid of Numeral.bin type
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-06-02 wenzelm 2006-06-02 misc cleanup;
2006-02-12 kleing 2006-02-12 * include generalised MVT in HyperReal (contributed by Benjamin Porter) * add non-denumerability of continuum in Real, includes closed intervals on real (contributed by Benjamin Porter, #22 in http://www.cs.ru.nl/~freek/100/)
2005-08-01 wenzelm 2005-08-01 simprocs: Simplifier.inherit_bounds;
2005-07-19 avigad 2005-07-19 added list of theorem changes to NEWS added real_of_int_abs to RealDef.thy
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-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-05-04 nipkow 2005-05-04 fixed lin.arith
2005-02-21 nipkow 2005-02-21 more fine tuniung
2004-10-05 paulson 2004-10-05 new simprules for abs and for things like a/b<1
2004-09-01 paulson 2004-09-01 new "respects" syntax for quotienting
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-07-29 paulson 2004-07-29 removal of more iff-rules from RealDef.thy
2004-07-29 paulson 2004-07-29 removed some [iff] declarations from RealDef.thy, concerning inequalities
2004-07-26 paulson 2004-07-26 converting Hyperreal/Transcendental to Isar script