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