| Fri, 19 Dec 2003 17:13:28 +0100 |
paulson |
tidying first part of HyperArith0.ML, using generic lemmas
|
file |
diff |
annotate
|
| Mon, 15 Dec 2003 16:38:25 +0100 |
paulson |
more general lemmas for Ring_and_Field
|
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, 12 Dec 2003 15:05:18 +0100 |
paulson |
moving some division theorems to Ring_and_Field
|
file |
diff |
annotate
|
| Wed, 10 Dec 2003 15:59:34 +0100 |
paulson |
Moving some theorems from Real/RealArith0.ML
|
file |
diff |
annotate
|
| Sun, 07 Dec 2003 16:30:06 +0100 |
paulson |
re-organisation of Real/RealArith0.ML; more `Isar scripts
|
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
|
| Thu, 04 Dec 2003 10:29:17 +0100 |
paulson |
Tidying of the integer development; towards removing the
|
file |
diff |
annotate
|
| Tue, 02 Dec 2003 11:48:15 +0100 |
paulson |
More re-organising of numerical theorems
|
file |
diff |
annotate
|
| Fri, 28 Nov 2003 12:09:37 +0100 |
paulson |
conversion of some Real theories to Isar scripts
|
file |
diff |
annotate
|
| Thu, 27 Nov 2003 10:47:55 +0100 |
paulson |
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
|
file |
diff |
annotate
|
| Tue, 25 Nov 2003 10:37:03 +0100 |
paulson |
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
|
file |
diff |
annotate
|
| Mon, 24 Nov 2003 15:33:07 +0100 |
paulson |
conversion of integers to use Ring_and_Field;
|
file |
diff |
annotate
|
| Fri, 21 Nov 2003 11:15:40 +0100 |
paulson |
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
|
file |
diff |
annotate
|