| Tue, 02 May 2000 18:42:48 +0200 |
paulson |
now with combine_numerals
|
file |
diff |
annotate
|
| Fri, 21 Apr 2000 11:29:33 +0200 |
paulson |
moved the simproc code to NatSimprocs.ML
|
file |
diff |
annotate
|
| Tue, 18 Apr 2000 15:53:50 +0200 |
paulson |
instantiates new simprocs for numerals of type "nat"
|
file |
diff |
annotate
|
| Thu, 13 Apr 2000 10:30:28 +0200 |
nipkow |
made mod_less_divisor a simplification rule.
|
file |
diff |
annotate
|
| Wed, 22 Mar 2000 13:01:18 +0100 |
paulson |
tidied using new "inst" rule
|
file |
diff |
annotate
|
| Mon, 13 Mar 2000 16:23:34 +0100 |
wenzelm |
case_tac now subsumes both boolean and datatype cases;
|
file |
diff |
annotate
|
| Mon, 13 Mar 2000 12:51:10 +0100 |
nipkow |
exhaust_tac -> cases_tac
|
file |
diff |
annotate
|
| Fri, 18 Feb 2000 18:29:28 +0100 |
nipkow |
installed lin arith for nat numerals.
|
file |
diff |
annotate
|
| Mon, 10 Jan 2000 16:07:29 +0100 |
nipkow |
int:nat->int is pushed inwards.
|
file |
diff |
annotate
|
| Wed, 24 Nov 1999 10:25:28 +0100 |
paulson |
tidied, choosing nicer names
|
file |
diff |
annotate
|
| Tue, 28 Sep 1999 15:31:54 +0200 |
paulson |
zero_is_mult, by symmetry
|
file |
diff |
annotate
|
| Wed, 08 Sep 1999 15:41:58 +0200 |
paulson |
simplification of relations involving 0, Suc and natural-number numerals
|
file |
diff |
annotate
|
| Thu, 29 Jul 1999 12:44:57 +0200 |
paulson |
added parentheses to cope with a possible reduction of the precedence of unary
|
file |
diff |
annotate
|
| Mon, 26 Jul 1999 16:32:23 +0200 |
paulson |
expandshort
|
file |
diff |
annotate
|
| Fri, 23 Jul 1999 17:27:48 +0200 |
paulson |
zmult_ac are no longer included by default
|
file |
diff |
annotate
|
| Wed, 21 Jul 1999 15:20:26 +0200 |
paulson |
more existing theorems renamed to use #0; also new results
|
file |
diff |
annotate
|
| Mon, 19 Jul 1999 15:27:34 +0200 |
paulson |
NatBin: binary arithmetic for the naturals
|
file |
diff |
annotate
|