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 replace type hypnat with nat star
2005-09-06 huffman 2005-09-06 replace type hypreal with real star
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-12-02 nipkow 2004-12-02 Added "ALL x > y" and relatives.
2004-11-23 nipkow 2004-11-23 added lemma
2004-10-19 paulson 2004-10-19 converted some induct_tac to induct
2004-10-12 paulson 2004-10-12 tweaks concerned with poly bug-fixing
2004-10-11 nipkow 2004-10-11 Proofs needed to be updated because induction now preserves name of induction variable.
2004-10-05 paulson 2004-10-05 new simprules for abs and for things like a/b<1
2004-10-01 paulson 2004-10-01 tweaking of arithmetic proofs
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-08-03 paulson 2004-08-03 new simprules Int_subset_iff and Un_subset_iff
2004-07-29 paulson 2004-07-29 removed some [iff] declarations from RealDef.thy, concerning inequalities
2004-07-28 paulson 2004-07-28 conversion of SEQ.ML to Isar script
2003-02-07 nipkow 2003-02-07 (*f -> ( *f because of new comments
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-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2000-12-30 paulson 2000-12-30 separation of HOL-Hyperreal from HOL-Real