Thu, 07 Mar 2002 23:41:30 +0100 | wenzelm | renamed nat_number_of to nat_number (avoid clash with separate theorem); | file | diff | annotate |
Mon, 25 Feb 2002 11:27:07 +0100 | berghofe | Introduced variants of operators + * ~ constrained to type int | file | diff | annotate |
Wed, 23 Jan 2002 16:58:05 +0100 | wenzelm | tuned; | file | diff | annotate |
Mon, 10 Dec 2001 15:23:19 +0100 | berghofe | Added code generator setup. | file | diff | annotate |
Tue, 07 Aug 2001 16:36:52 +0200 | paulson | Tweaks for 1 -> 1' | file | diff | annotate |
Mon, 06 Aug 2001 13:43:24 +0200 | nipkow | turned translation for 1::nat into def. | file | diff | annotate |
Fri, 01 Dec 2000 19:53:29 +0100 | nipkow | Linear arithmetic now copes with mixed nat/int formulae. | file | diff | annotate |
Thu, 03 Aug 2000 10:52:30 +0200 | paulson | introduction of integer exponentiation | file | diff | annotate |
Mon, 19 Jul 1999 15:27:34 +0200 | paulson | NatBin: binary arithmetic for the naturals | file | diff | annotate |