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