src/HOL/Hyperreal/HyperNat.thy
Wed, 15 Dec 2004 17:32:40 +0100 paulson removal of archaic Abs/Rep proofs
Tue, 19 Oct 2004 18:18:45 +0200 paulson converted some induct_tac to induct
Wed, 01 Sep 2004 15:04:01 +0200 paulson new "respects" syntax for quotienting
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Wed, 21 Jul 2004 08:35:29 +0200 nipkow Fixed latex problem
Fri, 16 Jul 2004 17:31:44 +0200 nipkow Corrected TeX problems.
Tue, 11 May 2004 20:11:08 +0200 obua changes made due to new Ring_and_Field theory
Sat, 01 May 2004 22:01:57 +0200 wenzelm tuned instance statements;
Fri, 23 Apr 2004 11:04:07 +0200 paulson congruent2 now allows different equiv relations
Mon, 15 Mar 2004 10:46:19 +0100 paulson heavy tidying
Mon, 01 Mar 2004 11:52:59 +0100 paulson converted Hyperreal/HTranscendental to Isar script
Thu, 26 Feb 2004 11:31:36 +0100 paulson converted Hyperreal/NatStar to Isar script
Tue, 10 Feb 2004 12:02:11 +0100 paulson generic of_nat and of_int functions, and generalization of iszero
Mon, 02 Feb 2004 12:23:46 +0100 paulson Conversion of HyperNat to Isar format and its declaration as a semiring
Thu, 08 Aug 2002 23:52:55 +0200 wenzelm tuned;
Mon, 08 Oct 2001 15:23:20 +0200 wenzelm sane numerals (stage 3): provide generic "1" on all number types;
Tue, 16 Jan 2001 12:20:52 +0100 paulson renamings: real_of_nat, real_of_int -> (overloaded) real
Tue, 09 Jan 2001 15:32:27 +0100 nipkow *** empty log message ***
Fri, 05 Jan 2001 18:48:18 +0100 nipkow ^^ -> ```
Thu, 04 Jan 2001 10:23:01 +0100 paulson more tidying, especially to remove real_of_posnat
Sat, 30 Dec 2000 22:03:47 +0100 paulson separation of HOL-Hyperreal from HOL-Real
less more (0) tip