src/HOL/Real/RealDef.thy
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
2004-07-01 paulson 2004-07-01 new treatment of binary numerals
2004-06-24 paulson 2004-06-24 replaced monomorphic abs definitions by abs_if
2004-05-18 obua 2004-05-18 Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
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-23 paulson 2004-04-23 congruent2 now allows different equiv relations
2004-03-30 paulson 2004-03-30 tidied
2004-03-25 paulson 2004-03-25 new treatment of equivalence classes
2004-03-19 paulson 2004-03-19 removed redundant thms
2004-03-08 paulson 2004-03-08 generic theorems about exponentials; general tidying up
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
2004-03-02 paulson 2004-03-02 fixed bugs in the setup of arithmetic procedures
2004-03-01 paulson 2004-03-01 new Ring_and_Field hierarchy, eliminating redundant axioms
2004-02-19 ballarin 2004-02-19 Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.
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-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