| Mon, 01 Aug 2005 19:20:26 +0200 |
wenzelm |
simprocs: Simplifier.inherit_bounds;
|
file |
diff |
annotate
|
| Fri, 29 Oct 2004 15:16:31 +0200 |
paulson |
fixed some awkward problems with nat/int simprocs
|
file |
diff |
annotate
|
| Tue, 11 May 2004 20:11:08 +0200 |
obua |
changes made due to new Ring_and_Field theory
|
file |
diff |
annotate
|
| Tue, 02 Mar 2004 11:06:37 +0100 |
paulson |
fixed bugs in the setup of arithmetic procedures
|
file |
diff |
annotate
|
| Tue, 17 Feb 2004 10:41:59 +0100 |
paulson |
further tweaks to the numeric theories
|
file |
diff |
annotate
|
| Sun, 15 Feb 2004 10:46:37 +0100 |
paulson |
Polymorphic treatment of binary arithmetic using axclasses
|
file |
diff |
annotate
|
| Tue, 10 Feb 2004 12:02:11 +0100 |
paulson |
generic of_nat and of_int functions, and generalization of iszero
|
file |
diff |
annotate
|
| Tue, 15 Jul 2003 15:20:54 +0200 |
paulson |
Fixing a simproc bug
|
file |
diff |
annotate
|
| Thu, 08 Aug 2002 23:50:23 +0200 |
wenzelm |
tuned prove_conv (error reporting done within meta_simplifier.ML);
|
file |
diff |
annotate
|
| Tue, 06 Aug 2002 11:22:05 +0200 |
wenzelm |
sane interface for simprocs;
|
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
|
| 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
|
| Thu, 21 Dec 2000 10:11:10 +0100 |
paulson |
simproc bug fix: negative literals and large terms
|
file |
diff |
annotate
|
| Tue, 19 Dec 2000 15:17:21 +0100 |
paulson |
inserting the simproc int_cancel_factor
|
file |
diff |
annotate
|
| Wed, 29 Nov 2000 10:21:43 +0100 |
paulson |
invoking CancelNumeralFactorFun
|
file |
diff |
annotate
|