| Tue, 18 May 2004 10:01:44 +0200 |
obua |
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
|
file |
diff |
annotate
|
| Tue, 11 May 2004 20:11:08 +0200 |
obua |
changes made due to new Ring_and_Field theory
|
file |
diff |
annotate
|
| Sat, 01 May 2004 22:01:57 +0200 |
wenzelm |
tuned instance statements;
|
file |
diff |
annotate
|
| Fri, 23 Apr 2004 11:04:07 +0200 |
paulson |
congruent2 now allows different equiv relations
|
file |
diff |
annotate
|
| Tue, 30 Mar 2004 11:25:14 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
| Thu, 25 Mar 2004 10:31:25 +0100 |
paulson |
new treatment of equivalence classes
|
file |
diff |
annotate
|
| Fri, 19 Mar 2004 10:50:06 +0100 |
paulson |
removed redundant thms
|
file |
diff |
annotate
|
| Mon, 08 Mar 2004 11:12:06 +0100 |
paulson |
generic theorems about exponentials; general tidying up
|
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
|
| Tue, 02 Mar 2004 11:06:37 +0100 |
paulson |
fixed bugs in the setup of arithmetic procedures
|
file |
diff |
annotate
|
| Mon, 01 Mar 2004 13:51:21 +0100 |
paulson |
new Ring_and_Field hierarchy, eliminating redundant axioms
|
file |
diff |
annotate
|
| Thu, 19 Feb 2004 15:57:34 +0100 |
ballarin |
Efficient, graph-based reasoner for linear and partial orders.
|
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
|
| Wed, 28 Jan 2004 17:01:01 +0100 |
paulson |
tidying up arithmetic for the hyperreals
|
file |
diff |
annotate
|