src/HOL/Hyperreal/HyperNat.thy
2007-10-20 chaieb 2007-10-20 fixed proofs
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
2006-12-16 huffman 2006-12-16 moved several theorems; rearranged theory dependencies
2006-12-16 huffman 2006-12-16 hypreal_of_hypnat abbreviates more general of_hypnat
2006-12-14 huffman 2006-12-14 remove ultra tactic and redundant FreeUltrafilterNat lemmas
2006-12-14 huffman 2006-12-14 redefine hSuc as *f* Suc, and move to HyperNat.thy
2006-12-12 huffman 2006-12-12 consistent naming for FreeUltrafilterNat lemmas; cleaned up
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-09-27 huffman 2006-09-27 reorganized HNatInfinite proofs; simplified and renamed some lemmas
2006-09-27 huffman 2006-09-27 hypreal_of_nat abbreviates of_nat
2006-09-24 huffman 2006-09-24 moved SEQ_Infinitesimal from SEQ to HyperNat
2006-09-16 huffman 2006-09-16 generalized types of many constants to work over arbitrary vector spaces; modified theorems using Rep_star to eliminate existential quantifiers
2006-06-02 wenzelm 2006-06-02 misc cleanup;
2006-04-09 wenzelm 2006-04-09 tuned syntax/abbreviations;
2005-09-16 huffman 2005-09-16 rearranged
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-12 huffman 2005-09-12 added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
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 replace type hypnat with nat star
2005-09-06 huffman 2005-09-06 replace type hypreal with real star
2004-12-15 paulson 2004-12-15 removal of archaic Abs/Rep proofs
2004-10-19 paulson 2004-10-19 converted some induct_tac to induct
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-21 nipkow 2004-07-21 Fixed latex problem
2004-07-16 nipkow 2004-07-16 Corrected TeX problems.
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-15 paulson 2004-03-15 heavy tidying
2004-03-01 paulson 2004-03-01 converted Hyperreal/HTranscendental to Isar script
2004-02-26 paulson 2004-02-26 converted Hyperreal/NatStar to Isar script
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
2002-08-08 wenzelm 2002-08-08 tuned;
2001-10-08 wenzelm 2001-10-08 sane numerals (stage 3): provide generic "1" on all number types;
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