src/HOL/Hyperreal/SEQ.thy
Fri, 01 Oct 2004 11:53:31 +0200 paulson tweaking of arithmetic proofs
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Tue, 03 Aug 2004 13:48:00 +0200 paulson new simprules Int_subset_iff and Un_subset_iff
Thu, 29 Jul 2004 16:14:42 +0200 paulson removed some [iff] declarations from RealDef.thy, concerning inequalities
Wed, 28 Jul 2004 16:26:27 +0200 paulson conversion of SEQ.ML to Isar script
Fri, 07 Feb 2003 16:40:23 +0100 nipkow (*f -> ( *f because of new comments
Fri, 02 Nov 2001 17:55:24 +0100 paulson Numerals and simprocs for types real and hypreal. The abstract
Fri, 05 Oct 2001 21:52:39 +0200 wenzelm sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
Sat, 30 Dec 2000 22:03:47 +0100 paulson separation of HOL-Hyperreal from HOL-Real
less more (0) tip