src/HOL/Hyperreal/HyperPow.thy
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-06-24 paulson 2004-06-24 replaced monomorphic abs definitions by abs_if
2004-03-15 paulson 2004-03-15 heavy tidying
2004-03-08 paulson 2004-03-08 generic theorems about exponentials; general tidying up
2004-03-05 paulson 2004-03-05 Conversion of Poly to Isar script, and other tidying of HOL/Hyperreal
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-09 paulson 2004-01-09 Defining the type class "ringpower" and deleting superseded theorems for types nat, int, real, hypreal
2001-10-08 wenzelm 2001-10-08 sane numerals (stage 3): provide generic "1" on all number types;
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