| Tue, 03 Oct 2000 18:45:36 +0200 |
wenzelm |
unsymbolize;
|
file |
diff |
annotate
|
| Wed, 13 Sep 2000 18:47:30 +0200 |
paulson |
more integer theorems, better simplification
|
file |
diff |
annotate
|
| Wed, 30 Aug 2000 16:29:21 +0200 |
nipkow |
introduced induct_thm_tac
|
file |
diff |
annotate
|
| Thu, 17 Aug 2000 11:55:47 +0200 |
paulson |
better rules for cancellation of common factors across comparisons
|
file |
diff |
annotate
|
| Thu, 03 Aug 2000 10:52:30 +0200 |
paulson |
introduction of integer exponentiation
|
file |
diff |
annotate
|
| Mon, 24 Jul 2000 23:51:46 +0200 |
wenzelm |
avoid referencing thy value;
|
file |
diff |
annotate
|
| Sun, 16 Jul 2000 20:56:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 22 Jun 2000 23:04:34 +0200 |
wenzelm |
bind_thm(s);
|
file |
diff |
annotate
|
| Wed, 14 Jun 2000 17:45:01 +0200 |
paulson |
new lemmas for signs of products
|
file |
diff |
annotate
|
| Mon, 22 May 2000 13:19:20 +0200 |
paulson |
further tidying
|
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
|
| Sun, 23 Apr 2000 11:34:41 +0200 |
paulson |
[Int_CC.sum_conv, Int_CC.rel_conv] no longer exist
|
file |
diff |
annotate
|
| Thu, 30 Mar 2000 19:45:51 +0200 |
nipkow |
recdef.rules -> recdef.simps
|
file |
diff |
annotate
|
| Fri, 18 Feb 2000 18:29:28 +0100 |
nipkow |
installed lin arith for nat numerals.
|
file |
diff |
annotate
|
| Tue, 21 Sep 1999 14:13:55 +0200 |
nipkow |
Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
|
file |
diff |
annotate
|
| Tue, 07 Sep 1999 10:40:58 +0200 |
wenzelm |
isatool expandshort;
|
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:12 +0200 |
paulson |
zadd_ac and zmult_ac are no longer included by default
|
file |
diff |
annotate
|
| Mon, 19 Jul 1999 15:30:59 +0200 |
paulson |
many new laws about div and mod
|
file |
diff |
annotate
|
| Wed, 14 Jul 1999 10:40:51 +0200 |
paulson |
optimization for division by powers of 2
|
file |
diff |
annotate
|
| Tue, 13 Jul 1999 10:45:09 +0200 |
paulson |
many new theorems
|
file |
diff |
annotate
|
| Fri, 09 Jul 1999 10:49:14 +0200 |
paulson |
faster division algorithm; monotonicity of div in 2nd arg
|
file |
diff |
annotate
|
| Thu, 08 Jul 1999 13:43:42 +0200 |
paulson |
Introduction of integer division algorithm
|
file |
diff |
annotate
|