| Fri, 17 Aug 2007 00:03:50 +0200 |
wenzelm |
proper signature for Meson;
|
file |
diff |
annotate
|
| Tue, 26 Jun 2007 18:32:53 +0200 |
paulson |
updated for metis method
|
file |
diff |
annotate
|
| Thu, 19 Apr 2007 18:23:11 +0200 |
paulson |
trying to make single-step proofs work better, especially if they contain
|
file |
diff |
annotate
|
| Tue, 09 Jan 2007 15:49:39 +0100 |
paulson |
simplified the resoution proofs
|
file |
diff |
annotate
|
| Thu, 04 Jan 2007 17:55:12 +0100 |
paulson |
improvements to proof reconstruction. Some files loaded in a different order
|
file |
diff |
annotate
|
| Fri, 22 Dec 2006 21:00:55 +0100 |
paulson |
revised for new make_clauses
|
file |
diff |
annotate
|
| Mon, 23 Oct 2006 11:18:50 +0200 |
paulson |
new single-step proofs
|
file |
diff |
annotate
|
| Fri, 20 Oct 2006 11:07:45 +0200 |
paulson |
example of a single-step proof reconstruction
|
file |
diff |
annotate
|
| Wed, 14 Dec 2005 16:14:41 +0100 |
paulson |
modified example for new clauses
|
file |
diff |
annotate
|
| Tue, 28 Jun 2005 17:56:04 +0200 |
paulson |
stylistic improvements
|
file |
diff |
annotate
|
| Fri, 24 Jun 2005 17:25:10 +0200 |
paulson |
meson method taking an argument list
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Fri, 20 May 2005 18:34:14 +0200 |
paulson |
converted some problems to Isar format
|
file |
diff |
annotate
|
| Tue, 07 Dec 2004 18:10:13 +0100 |
paulson |
renamed attributes to lower case
|
file |
diff |
annotate
|
| Fri, 20 Aug 2004 12:21:03 +0200 |
paulson |
proof reconstruction for external ATPs
|
file |
diff |
annotate
|
| Fri, 06 Aug 2004 13:35:26 +0200 |
paulson |
modified resolution proof
|
file |
diff |
annotate
|
| Mon, 28 Jun 2004 11:15:13 +0200 |
paulson |
new method for explicit classical resolution
|
file |
diff |
annotate
|
| Wed, 29 Oct 2003 16:16:20 +0100 |
paulson |
tidying
|
file |
diff |
annotate
|
| Wed, 08 Oct 2003 15:57:41 +0200 |
paulson |
Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
|
file |
diff |
annotate
|