| Tue, 23 Dec 2003 14:46:08 +0100 |
paulson |
new theorems
|
file |
diff |
annotate
|
| Mon, 22 Dec 2003 12:50:01 +0100 |
paulson |
removing obsolete bindings
|
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
|
| Thu, 11 Dec 2003 10:52:41 +0100 |
paulson |
removal of abel_cancel from Real
|
file |
diff |
annotate
|
| Wed, 10 Dec 2003 15:59:34 +0100 |
paulson |
Moving some theorems from Real/RealArith0.ML
|
file |
diff |
annotate
|
| Fri, 05 Dec 2003 10:28:02 +0100 |
paulson |
Converting more of the "real" development to Isar scripts
|
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, 21 Dec 2000 18:57:12 +0100 |
nipkow |
rational linear arithmetic
|
file |
diff |
annotate
|
| Fri, 01 Dec 2000 19:53:29 +0100 |
nipkow |
Linear arithmetic now copes with mixed nat/int formulae.
|
file |
diff |
annotate
|
| Tue, 25 Jul 2000 00:06:46 +0200 |
wenzelm |
rearranged setup of arithmetic procedures, avoiding global reference values;
|
file |
diff |
annotate
|