| Thu, 30 May 2002 10:12:52 +0200 |
nipkow |
Modifications due to enhanced linear arithmetic.
|
file |
diff |
annotate
|
| Thu, 13 Dec 2001 15:45:03 +0100 |
wenzelm |
isatool expandshort;
|
file |
diff |
annotate
|
| Fri, 02 Nov 2001 17:55:24 +0100 |
paulson |
Numerals and simprocs for types real and hypreal. The abstract
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 11:54:22 +0200 |
paulson |
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 22:08:29 +0200 |
wenzelm |
moved rulify to ObjectLogic;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2001 00:02:46 +0200 |
wenzelm |
* sane numerals (stage 2): plain "num" syntax (removed "#");
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Tue, 19 Dec 2000 15:16:21 +0100 |
paulson |
new simprule zero_less_abs_iff
|
file |
diff |
annotate
|
| Tue, 12 Dec 2000 11:58:44 +0100 |
paulson |
greater use of overloaded rules (order_less_imp_le not zless_imp_zle, ...)
|
file |
diff |
annotate
|
| Sat, 18 Nov 2000 19:45:37 +0100 |
wenzelm |
abs_eq_0: #0 instead of 0;
|
file |
diff |
annotate
|
| Thu, 16 Nov 2000 19:01:39 +0100 |
wenzelm |
added abs_mult, abs_eq_0, square_nonzero;
|
file |
diff |
annotate
|
| Tue, 17 Oct 2000 08:00:46 +0200 |
nipkow |
added intermediate value thms
|
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
|
| 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
|