| 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 |