Thu, 21 Dec 2000 18:08:10 +0100 |
paulson |
further tidying of NSA proofs
|
file |
diff |
annotate
|
Wed, 20 Dec 2000 12:15:52 +0100 |
paulson |
further tidying
|
file |
diff |
annotate
|
Tue, 19 Dec 2000 15:06:59 +0100 |
paulson |
more tidying
|
file |
diff |
annotate
|
Mon, 18 Dec 2000 12:21:54 +0100 |
paulson |
loads the new simproc extract_common_term
|
file |
diff |
annotate
|
Fri, 15 Dec 2000 17:41:38 +0100 |
paulson |
further round of tidying
|
file |
diff |
annotate
|
Thu, 14 Dec 2000 10:30:11 +0100 |
paulson |
new theorem real_lbound_gt_zero
|
file |
diff |
annotate
|
Wed, 13 Dec 2000 10:34:45 +0100 |
paulson |
another round of tidying-up
|
file |
diff |
annotate
|
Tue, 12 Dec 2000 12:01:19 +0100 |
paulson |
first stage in tidying up Real and Hyperreal.
|
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
|