| Tue, 19 Dec 2000 15:17:53 +0100 | paulson | inserting the simproc nat_cancel_factor | file | diff | annotate |
| Mon, 18 Dec 2000 14:59:05 +0100 | nipkow | moved mk_bin from Numerals to HOLogic | file | diff | annotate |
| Fri, 01 Dec 2000 19:53:29 +0100 | nipkow | Linear arithmetic now copes with mixed nat/int formulae. | file | diff | annotate |
| Wed, 29 Nov 2000 10:21:43 +0100 | paulson | invoking CancelNumeralFactorFun | file | diff | annotate |
| Thu, 10 Aug 2000 11:30:22 +0200 | paulson | new structure field "add" for CombineNumerals | file | diff | annotate |
| Mon, 07 Aug 2000 10:27:11 +0200 | paulson | added a dummy "thm list" argument to prove_conv for the new interface to | file | diff | annotate |
| Tue, 25 Jul 2000 00:06:46 +0200 | wenzelm | rearranged setup of arithmetic procedures, avoiding global reference values; | file | diff | annotate |