src/HOL/Hyperreal/HSeries.ML
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-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-06-25 paulson 2001-06-25 Simprocs for type "nat" no longer introduce numerals unless they are already present in the expression, and in a coefficient position (i.e. as a factor of a monomial).
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