| Fri, 28 Oct 2005 08:40:55 +0200 |
haftmann |
reachable - abandoned foldl_map in favor of fold_map
|
changeset |
files
|
| Fri, 28 Oct 2005 02:30:53 +0200 |
mengj |
Added Tools/res_hol_clause.ML
|
changeset |
files
|
| Fri, 28 Oct 2005 02:30:12 +0200 |
mengj |
Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.
|
changeset |
files
|
| Fri, 28 Oct 2005 02:29:01 +0200 |
mengj |
Added "writeln_strs" to the signature
|
changeset |
files
|
| Fri, 28 Oct 2005 02:28:20 +0200 |
mengj |
Added several new functions that are used to prove HOL goals. Added new methods "vampireH" and "eproverH" that can prove both FOL and HOL goals. The old "vampire" and "eprover" methods are renamed to "vampireF" and "eproverF"; they can only prove FOL goals.
|
changeset |
files
|
| Fri, 28 Oct 2005 02:27:19 +0200 |
mengj |
Added new functions to handle HOL goals and lemmas.
|
changeset |
files
|
| Fri, 28 Oct 2005 02:25:57 +0200 |
mengj |
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
|
changeset |
files
|
| Fri, 28 Oct 2005 02:24:58 +0200 |
mengj |
Added several functions to the signature.
|
changeset |
files
|
| Fri, 28 Oct 2005 02:23:49 +0200 |
mengj |
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
|
changeset |
files
|
| Thu, 27 Oct 2005 18:25:33 +0200 |
paulson |
sorted lemma lists
|
changeset |
files
|
| Thu, 27 Oct 2005 13:59:06 +0200 |
wenzelm |
* HOL: alternative iff syntax;
|
changeset |
files
|
| Thu, 27 Oct 2005 13:54:43 +0200 |
wenzelm |
consts: monomorphic;
|
changeset |
files
|
| Thu, 27 Oct 2005 13:54:42 +0200 |
wenzelm |
removed inappropriate monomorphic test;
|
changeset |
files
|
| Thu, 27 Oct 2005 13:54:40 +0200 |
wenzelm |
replaced Defs.monomorphic by Sign.monomorphic;
|
changeset |
files
|