| Fri, 05 Dec 2003 19:39:39 +0100 |
skalberg |
Added lazy sequences and parser combinators for same.
|
changeset |
files
|
| Fri, 05 Dec 2003 18:10:59 +0100 |
paulson |
more field division lemmas transferred from Real to Ring_and_Field
|
changeset |
files
|
| Fri, 05 Dec 2003 12:58:18 +0100 |
paulson |
stylistic changes
|
changeset |
files
|
| Fri, 05 Dec 2003 10:28:02 +0100 |
paulson |
Converting more of the "real" development to Isar scripts
|
changeset |
files
|
| Thu, 04 Dec 2003 21:57:15 +0100 |
nipkow |
hide Push
|
changeset |
files
|
| Thu, 04 Dec 2003 16:16:36 +0100 |
paulson |
further simplifications of the integer development; converting more .ML files
|
changeset |
files
|
| Thu, 04 Dec 2003 10:29:17 +0100 |
paulson |
Tidying of the integer development; towards removing the
|
changeset |
files
|
| Wed, 03 Dec 2003 10:49:34 +0100 |
paulson |
Simplification of the development of Integers
|
changeset |
files
|
| Tue, 02 Dec 2003 11:48:15 +0100 |
paulson |
More re-organising of numerical theorems
|
changeset |
files
|
| Fri, 28 Nov 2003 12:09:37 +0100 |
paulson |
conversion of some Real theories to Isar scripts
|
changeset |
files
|
| Thu, 27 Nov 2003 10:47:55 +0100 |
paulson |
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
|
changeset |
files
|
| Tue, 25 Nov 2003 10:37:03 +0100 |
paulson |
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
|
changeset |
files
|
| Mon, 24 Nov 2003 15:33:07 +0100 |
paulson |
conversion of integers to use Ring_and_Field;
|
changeset |
files
|
| Fri, 21 Nov 2003 11:15:40 +0100 |
paulson |
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
|
changeset |
files
|