| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Thu, 26 May 2005 16:50:20 +0200 |
paulson |
goodby to modUnix
|
file |
diff |
annotate
|
| Mon, 23 May 2005 00:18:51 +0200 |
quigley |
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
|
file |
diff |
annotate
|
| Thu, 19 May 2005 11:08:15 +0200 |
paulson |
Skolemization of simprules and classical rules
|
file |
diff |
annotate
|
| Thu, 28 Apr 2005 17:56:58 +0200 |
paulson |
fixed treatment of higher-order simprules
|
file |
diff |
annotate
|
| Tue, 19 Apr 2005 18:08:44 +0200 |
paulson |
more tidying of libraries in Reconstruction
|
file |
diff |
annotate
|
| Tue, 12 Apr 2005 11:08:25 +0200 |
paulson |
tweaks mainly to achieve sml/nj compatibility
|
file |
diff |
annotate
|
| Fri, 08 Apr 2005 18:43:39 +0200 |
paulson |
Reconstruction code, now packaged to avoid name clashes
|
file |
diff |
annotate
|
| Fri, 08 Apr 2005 10:50:02 +0200 |
paulson |
temporarily removed ATP code
|
file |
diff |
annotate
|
| Thu, 07 Apr 2005 17:45:51 +0200 |
quigley |
Reconstruction.thy and IsaMakefile updated
|
file |
diff |
annotate
|
| Mon, 04 Apr 2005 18:43:18 +0200 |
quigley |
Updated to add watcher code.
|
file |
diff |
annotate
|
| Fri, 01 Apr 2005 11:12:39 +0200 |
paulson |
patch to get it working again
|
file |
diff |
annotate
|
| Tue, 07 Dec 2004 16:16:10 +0100 |
paulson |
all theories must be related to Reconstruction
|
file |
diff |
annotate
|
| Thu, 02 Dec 2004 11:09:19 +0100 |
paulson |
new CLAUSIFY attribute for proof reconstruction with lemmas
|
file |
diff |
annotate
|
| Fri, 20 Aug 2004 12:21:03 +0200 |
paulson |
proof reconstruction for external ATPs
|
file |
diff |
annotate
|