Wed, 13 Sep 2000 18:47:30 +0200 |
paulson |
more integer theorems, better simplification
|
file |
diff |
annotate
|
Thu, 17 Aug 2000 11:55:47 +0200 |
paulson |
better rules for cancellation of common factors across comparisons
|
file |
diff |
annotate
|
Mon, 24 Jul 2000 23:57:02 +0200 |
wenzelm |
avoid referencing thy value;
|
file |
diff |
annotate
|
Thu, 22 Jun 2000 23:04:34 +0200 |
wenzelm |
bind_thm(s);
|
file |
diff |
annotate
|
Wed, 14 Jun 2000 17:46:10 +0200 |
paulson |
tidied a proof using new lemmas for signs of products
|
file |
diff |
annotate
|
Tue, 23 May 2000 18:06:22 +0200 |
paulson |
added type constraint ::nat because 0 is now overloaded
|
file |
diff |
annotate
|
Fri, 12 May 2000 15:11:42 +0200 |
paulson |
tidying, especially to remove zcompare_rls from proofs
|
file |
diff |
annotate
|
Fri, 05 May 2000 17:49:34 +0200 |
paulson |
new lemmas about binary division
|
file |
diff |
annotate
|
Thu, 04 May 2000 18:39:51 +0200 |
paulson |
a safer way of proving literal equalities
|
file |
diff |
annotate
|
Thu, 04 May 2000 15:16:18 +0200 |
paulson |
new lemmas concerning powers and #mmm
|
file |
diff |
annotate
|
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
|