| Fri, 26 Aug 2005 10:01:06 +0200 |
ballarin |
Lemmas on dvd, power and finite summation added or strengthened.
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 18:53:11 +0200 |
paulson |
more simprules now have names
|
file |
diff |
annotate
|
| Tue, 12 Jul 2005 17:56:03 +0200 |
avigad |
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Thu, 07 Oct 2004 15:42:30 +0200 |
paulson |
simplification tweaks for better arithmetic reasoning
|
file |
diff |
annotate
|
| Mon, 04 Oct 2004 15:28:03 +0200 |
paulson |
revised simprules for division
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Fri, 16 Apr 2004 04:07:10 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Fri, 19 Mar 2004 10:48:22 +0100 |
paulson |
new thms
|
file |
diff |
annotate
|
| Fri, 05 Mar 2004 15:19:55 +0100 |
paulson |
some new results
|
file |
diff |
annotate
|
| Thu, 04 Mar 2004 12:06:07 +0100 |
paulson |
new material from Avigad, and simplified treatment of division by 0
|
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
|
| Mon, 12 Jan 2004 16:51:45 +0100 |
paulson |
Added lemmas to Ring_and_Field with slightly modified simplification rules
|
file |
diff |
annotate
|
| Wed, 10 Dec 2003 15:59:34 +0100 |
paulson |
Moving some theorems from Real/RealArith0.ML
|
file |
diff |
annotate
|
| Thu, 04 Dec 2003 16:16:36 +0100 |
paulson |
further simplifications of the integer development; converting more .ML files
|
file |
diff |
annotate
|
| Thu, 24 Jul 2003 16:41:40 +0200 |
paulson |
header comment
|
file |
diff |
annotate
|
| Wed, 29 Nov 2000 10:21:43 +0100 |
paulson |
invoking CancelNumeralFactorFun
|
file |
diff |
annotate
|
| Tue, 25 Jul 2000 00:06:46 +0200 |
wenzelm |
rearranged setup of arithmetic procedures, avoiding global reference values;
|
file |
diff |
annotate
|
| Fri, 12 May 2000 14:57:28 +0200 |
paulson |
new dummy theory; prevents strange errors when loading NatSimprocs.ML
|
file |
diff |
annotate
|