| Mon, 06 Aug 2001 13:43:24 +0200 | nipkow | turned translation for 1::nat into def. | file | diff | annotate |
| Thu, 01 Feb 2001 20:43:41 +0100 | wenzelm | added "numerals" theorems; | file | diff | annotate |
| Mon, 22 Jan 2001 11:45:57 +0100 | paulson | deleted obsolete theorems | file | diff | annotate |
| Sat, 30 Dec 2000 22:19:30 +0100 | paulson | now #16*(x+y) distributes for nat just as for other numeric types | file | diff | annotate |
| Wed, 20 Dec 2000 12:14:26 +0100 | paulson | tidying, removing obsolete lemmas about 0=... and 1=... | 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 |