| 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
|
| Thu, 27 Oct 2005 13:54:38 +0200 |
wenzelm |
alternative iff syntax for equality on booleans, with print_mode 'iff';
|
changeset |
files
|
| Thu, 27 Oct 2005 08:14:05 +0200 |
haftmann |
added module Pure/General/rat.ML
|
changeset |
files
|
| Wed, 26 Oct 2005 16:31:53 +0200 |
paulson |
tidied away duplicate thm
|
changeset |
files
|
| Tue, 25 Oct 2005 18:38:21 +0200 |
wenzelm |
EVERY;
|
changeset |
files
|
| Tue, 25 Oct 2005 18:18:59 +0200 |
wenzelm |
traceIt: plain term;
|
changeset |
files
|
| Tue, 25 Oct 2005 18:18:58 +0200 |
wenzelm |
val legacy = ref false;
|
changeset |
files
|
| Tue, 25 Oct 2005 18:18:57 +0200 |
wenzelm |
prove_raw: cterms, explicit asms;
|
changeset |
files
|
| Tue, 25 Oct 2005 18:18:49 +0200 |
wenzelm |
avoid legacy goals;
|
changeset |
files
|
| Sat, 22 Oct 2005 01:22:10 +0200 |
wenzelm |
legacy = ref true for the time being -- avoid volumious warnings;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:20:29 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:17:00 +0200 |
wenzelm |
avoid OldGoals shortcuts;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:16:57 +0200 |
wenzelm |
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
|
changeset |
files
|
| Fri, 21 Oct 2005 18:15:00 +0200 |
wenzelm |
Internal goals.
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:59 +0200 |
wenzelm |
renamed triv_goal to goalI, rev_triv_goal to goalD;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:58 +0200 |
wenzelm |
tuned header;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:57 +0200 |
wenzelm |
Goal.norm_hhf_rule;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:56 +0200 |
wenzelm |
export add_binds_i;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:55 +0200 |
wenzelm |
load_file: setmp OldGoals.legacy true;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:54 +0200 |
wenzelm |
improved check_result;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:53 +0200 |
wenzelm |
Goal.prove_plain;
|
changeset |
files
|