src/HOL/Hyperreal/Lim.ML
Fri, 07 Feb 2003 16:40:23 +0100 nipkow (*f -> ( *f because of new comments
Tue, 08 Oct 2002 08:20:17 +0200 nipkow Got rid of rotates because of new simplifier
Mon, 30 Sep 2002 16:14:02 +0200 berghofe Adapted to new simplifier.
Thu, 13 Dec 2001 15:45:03 +0100 wenzelm isatool expandshort;
Wed, 12 Dec 2001 19:21:02 +0100 nipkow mods due to reorienting and renaming of real_minus_mult_eq1/2
Fri, 02 Nov 2001 17:55:24 +0100 paulson Numerals and simprocs for types real and hypreal. The abstract
Mon, 08 Oct 2001 15:23:20 +0200 wenzelm sane numerals (stage 3): provide generic "1" on all number types;
Sat, 06 Oct 2001 00:02:46 +0200 wenzelm * sane numerals (stage 2): plain "num" syntax (removed "#");
Fri, 05 Oct 2001 21:52:39 +0200 wenzelm sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
Tue, 07 Aug 2001 16:36:52 +0200 paulson Tweaks for 1 -> 1'
Tue, 26 Jun 2001 17:05:10 +0200 paulson tidied
Thu, 22 Feb 2001 11:31:31 +0100 paulson a PROPER tidy-up
Wed, 21 Feb 2001 12:07:00 +0100 oheimb added split_conv_tac (also to claset()) as an optimization
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