| Thu, 13 Dec 2001 15:45:03 +0100 |
wenzelm |
isatool expandshort;
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 11:54:22 +0200 |
paulson |
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
|
file |
diff |
annotate
|
| Sat, 06 Oct 2001 00:02:46 +0200 |
wenzelm |
* sane numerals (stage 2): plain "num" syntax (removed "#");
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
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, 11 May 2001 13:49:15 +0200 |
nipkow |
added mult_Suc laws to lin.arith.simpset.
|
file |
diff |
annotate
|
| Thu, 19 Apr 2001 13:36:07 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Sat, 12 Aug 2000 21:42:12 +0200 |
paulson |
some ad-hoc simprules for div and mod to reduce the
|
file |
diff |
annotate
|
| Tue, 25 Jul 2000 00:06:46 +0200 |
wenzelm |
rearranged setup of arithmetic procedures, avoiding global reference values;
|
file |
diff |
annotate
|
| Tue, 30 May 2000 16:08:38 +0200 |
wenzelm |
cleaned up;
|
file |
diff |
annotate
|
| Tue, 23 May 2000 18:06:22 +0200 |
paulson |
added type constraint ::nat because 0 is now overloaded
|
file |
diff |
annotate
|
| Tue, 16 May 2000 14:07:06 +0200 |
paulson |
new policy to simplify the use of numerals:
|
file |
diff |
annotate
|
| Fri, 12 May 2000 15:14:08 +0200 |
paulson |
new simprules for nat_case and nat_rec
|
file |
diff |
annotate
|
| Wed, 10 May 2000 13:36:27 +0200 |
paulson |
new default simprule for better compatibility with old setup
|
file |
diff |
annotate
|
| Fri, 05 May 2000 17:49:54 +0200 |
paulson |
simprocs now simplify the RHS of their result
|
file |
diff |
annotate
|
| Thu, 04 May 2000 12:29:00 +0200 |
paulson |
further tidying of integer simprocs
|
file |
diff |
annotate
|
| Wed, 03 May 2000 18:33:28 +0200 |
paulson |
Installation of CombineNumerals for the integers
|
file |
diff |
annotate
|
| Tue, 02 May 2000 18:42:48 +0200 |
paulson |
now with combine_numerals
|
file |
diff |
annotate
|
| Sun, 23 Apr 2000 11:35:00 +0200 |
paulson |
bug fixes to new simprocs
|
file |
diff |
annotate
|
| Fri, 21 Apr 2000 11:29:57 +0200 |
paulson |
new file containing simproc invocations, from NatBin.ML
|
file |
diff |
annotate
|