src/HOL/Hyperreal/HyperDef.thy
2006-04-09 wenzelm 2006-04-09 tuned syntax/abbreviations;
2005-09-15 huffman 2005-09-15 merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
2005-09-09 huffman 2005-09-09 starfun, starset, and other functions on NS types are now polymorphic; many similar theorems have been generalized and merged; (star_n X) replaces (Abs_star(starrel `` {X})); many proofs have been simplified with the transfer tactic.
2005-09-07 huffman 2005-09-07 added theorem hypreal_inverse2
2005-09-06 huffman 2005-09-06 replace type hypreal with real star
2005-09-06 huffman 2005-09-06 reimplement Filter.thy with locales
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-02-21 nipkow 2005-02-21 comprehensive cleanup, replacing sumr by setsum
2004-12-15 paulson 2004-12-15 removal of archaic Abs/Rep proofs
2004-10-07 paulson 2004-10-07 simplification tweaks for better arithmetic reasoning
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 removed some [iff] declarations from RealDef.thy, concerning inequalities
2004-07-11 wenzelm 2004-07-11 local_cla/simpset_of;
2004-07-01 paulson 2004-07-01 new treatment of binary numerals
2004-05-11 obua 2004-05-11 changes made due to new Ring_and_Field theory
2004-05-06 paulson 2004-05-06 tidied
2004-05-01 wenzelm 2004-05-01 tuned instance statements;
2004-04-23 paulson 2004-04-23 congruent2 now allows different equiv relations
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2004-03-19 paulson 2004-03-19 conversion of Hyperreal/Lim to new-style
2004-03-15 paulson 2004-03-15 heavy tidying
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
2004-03-01 paulson 2004-03-01 new Ring_and_Field hierarchy, eliminating redundant axioms
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-02-02 paulson 2004-02-02 Conversion of HyperNat to Isar format and its declaration as a semiring
2004-01-29 paulson 2004-01-29 simplifications in the hyperreals
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
2004-01-26 schirmer 2004-01-26 * Support for raw latex output in control symbols: \<^raw...> * Symbols may only start with one backslash: \<...>. \\<...> is no longer accepted by the scanner. - Adapted some Isar-theories to fit to this policy
2004-01-09 paulson 2004-01-09 Defining the type class "ringpower" and deleting superseded theorems for types nat, int, real, hypreal
2004-01-06 paulson 2004-01-06 Ring_and_Field now requires axiom add_left_imp_eq for semirings. This allows more theorems to be proved for semirings, but requires a redundant axiom to be proved for rings, etc.
2004-01-01 paulson 2004-01-01 tweaking of lemmas in RealDef, RealOrd
2003-12-27 paulson 2003-12-27 re-organized numeric lemmas
2003-12-25 paulson 2003-12-25 re-organized some hyperreal and real lemmas
2003-12-19 paulson 2003-12-19 tidying first part of HyperArith0.ML, using generic lemmas
2003-12-18 paulson 2003-12-18 tidied
2003-12-17 paulson 2003-12-17 converted Hyperreal/HyperDef to Isar script
2002-08-08 wenzelm 2002-08-08 tuned;
2001-11-02 paulson 2001-11-02 Numerals and simprocs for types real and hypreal. The abstract constants 0, 1 and binary numerals work harmoniously.
2001-10-08 wenzelm 2001-10-08 sane numerals (stage 3): provide generic "1" on all number types;
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-01-16 paulson 2001-01-16 renamings: real_of_nat, real_of_int -> (overloaded) real inf_close -> approx SReal -> Reals SNat -> Nats
2001-01-09 nipkow 2001-01-09 *** empty log message ***
2001-01-05 nipkow 2001-01-05 ^^ -> ``` Univalent -> single_valued
2001-01-04 paulson 2001-01-04 more tidying, especially to remove real_of_posnat
2000-12-30 paulson 2000-12-30 separation of HOL-Hyperreal from HOL-Real