| Wed, 14 Dec 2005 01:39:41 +0100 |
mengj |
changed ATP input files' names and location.
|
file |
diff |
annotate
|
| Tue, 06 Dec 2005 06:22:14 +0100 |
mengj |
Added more functions for new type embedding of HOL clauses.
|
file |
diff |
annotate
|
| Mon, 28 Nov 2005 07:15:13 +0100 |
mengj |
Added in four control flags for HOL and FOL translations.
|
file |
diff |
annotate
|
| Fri, 18 Nov 2005 07:07:47 +0100 |
mengj |
-- added combinator reduction axioms (typed and untyped) for HOL goals.
|
file |
diff |
annotate
|
| Wed, 09 Nov 2005 18:01:33 +0100 |
paulson |
Skolemization by inference, but not quite finished
|
file |
diff |
annotate
|
| Thu, 03 Nov 2005 04:31:12 +0100 |
mengj |
Changed the way additional lemmas are passed to ATP methods for proof of a goal: now only list them after the methods' names.
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 17:27:49 +0200 |
haftmann |
circumvented smlnj value restriction
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 02:27:19 +0200 |
mengj |
Added new functions to handle HOL goals and lemmas.
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 02:57:22 +0200 |
mengj |
Merged theory ResAtpOracle.thy into ResAtpMethods.thy
|
file |
diff |
annotate
|
| Wed, 19 Oct 2005 10:25:46 +0200 |
mengj |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 19 Oct 2005 06:33:24 +0200 |
mengj |
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
|
file |
diff |
annotate
|