| Wed, 19 Dec 2007 17:40:48 +0100 |
paulson |
Replaced refs by config params; finer critical section in mets method
|
file |
diff |
annotate
|
| Mon, 10 Dec 2007 11:24:06 +0100 |
haftmann |
explicit import of theory Main
|
file |
diff |
annotate
|
| Tue, 06 Nov 2007 08:47:30 +0100 |
haftmann |
removed subclass edge ordered_ring < lordered_ring
|
file |
diff |
annotate
|
| Thu, 18 Oct 2007 17:38:45 +0200 |
paulson |
some more metis calls
|
file |
diff |
annotate
|
| Thu, 18 Oct 2007 16:09:36 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Wed, 10 Oct 2007 15:05:34 +0200 |
paulson |
more metis proofs
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 18:14:00 +0200 |
paulson |
context-based treatment of generalization; also handling TFrees in axiom clauses
|
file |
diff |
annotate
|
| Fri, 05 Oct 2007 09:59:21 +0200 |
paulson |
metis method: used theorems
|
file |
diff |
annotate
|
| Thu, 06 Sep 2007 16:54:03 +0200 |
paulson |
new proofs found
|
file |
diff |
annotate
|
| Mon, 16 Jul 2007 19:18:23 +0200 |
paulson |
tidied using sledgehammer
|
file |
diff |
annotate
|
| Fri, 29 Jun 2007 18:21:25 +0200 |
paulson |
bug fixes to proof reconstruction
|
file |
diff |
annotate
|
| Sat, 23 Jun 2007 19:33:22 +0200 |
nipkow |
tuned and renamed group_eq_simps and ring_eq_simps
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 20:07:26 +0200 |
wenzelm |
tuned proofs -- avoid implicit prems;
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 13:23:33 +0200 |
paulson |
integration of Metis prover
|
file |
diff |
annotate
|