| Tue, 25 Jul 2000 00:06:46 +0200 |
wenzelm |
rearranged setup of arithmetic procedures, avoiding global reference values;
|
file |
diff |
annotate
|
| Thu, 06 Jul 2000 15:38:26 +0200 |
nipkow |
added zabs to arith_tac
|
file |
diff |
annotate
|
| Sat, 01 Jul 2000 17:52:52 +0200 |
nipkow |
Defined abs on int.
|
file |
diff |
annotate
|
| Fri, 16 Jun 2000 13:21:17 +0200 |
paulson |
some missing simprules for integer linear arithmetic
|
file |
diff |
annotate
|
| Wed, 14 Jun 2000 17:45:01 +0200 |
paulson |
new lemmas for signs of products
|
file |
diff |
annotate
|
| Tue, 30 May 2000 16:08:38 +0200 |
wenzelm |
cleaned up;
|
file |
diff |
annotate
|
| Mon, 08 May 2000 16:58:44 +0200 |
paulson |
better simplification of the result of simprocs
|
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 18:40:57 +0200 |
paulson |
if_weak_cong should make linear arithmetic faster
|
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:33:41 +0200 |
paulson |
now uses the new cancel_numerals simproc
|
file |
diff |
annotate
|
| Fri, 18 Feb 2000 18:29:28 +0100 |
nipkow |
installed lin arith for nat numerals.
|
file |
diff |
annotate
|
| Mon, 04 Oct 1999 21:48:23 +0200 |
wenzelm |
simprocs now in IntArith;
|
file |
diff |
annotate
|