src/HOL/Hyperreal/Integration.ML
Wed, 28 Jul 2004 16:26:27 +0200 paulson conversion of SEQ.ML to Isar script
Wed, 28 Jul 2004 10:49:29 +0200 paulson conversion of Hyperreal/MacLaurin_lemmas to Isar script
Fri, 19 Mar 2004 10:51:03 +0100 paulson conversion of Hyperreal/Lim to new-style
Fri, 05 Mar 2004 15:18:59 +0100 paulson Conversion of Poly to Isar script, and other tidying of HOL/Hyperreal
Sun, 15 Feb 2004 10:46:37 +0100 paulson Polymorphic treatment of binary arithmetic using axclasses
Tue, 27 Jan 2004 15:39:51 +0100 paulson replacing HOL/Real/PRat, PNat by the rational number development
Sat, 03 Jan 2004 16:09:39 +0100 paulson Deleting more redundant theorems
Thu, 01 Jan 2004 10:06:32 +0100 paulson tweaking of lemmas in RealDef, RealOrd
Thu, 25 Dec 2003 22:48:32 +0100 paulson re-organized some hyperreal and real lemmas
Fri, 19 Dec 2003 17:13:28 +0100 paulson tidying first part of HyperArith0.ML, using generic lemmas
Sat, 13 Dec 2003 09:33:52 +0100 paulson absolute value theorems moved to HOL/Ring_and_Field
Fri, 05 Dec 2003 18:10:59 +0100 paulson more field division lemmas transferred from Real to Ring_and_Field
Mon, 05 May 2003 18:23:40 +0200 paulson New material on integration, etc. Moving Hyperreal/ex
less more (0) tip