src/HOL/Hyperreal/Lim.thy
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-28 paulson 2004-07-28 fixed precedences
2004-07-28 paulson 2004-07-28 conversion of Hyperreal/MacLaurin_lemmas to Isar script
2004-07-26 paulson 2004-07-26 converting Hyperreal/Transcendental to Isar script
2004-06-24 paulson 2004-06-24 replaced monomorphic abs definitions by abs_if
2004-03-19 paulson 2004-03-19 conversion of Hyperreal/Lim to new-style
2004-02-15 paulson 2004-02-15 Polymorphic treatment of binary arithmetic using axclasses
2003-11-28 paulson 2003-11-28 conversion of some Real theories to Isar scripts
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-06 wenzelm 2001-10-06 * sane numerals (stage 2): plain "num" syntax (removed "#");
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