mengj [Fri, 28 Oct 2005 02:28:20 +0200] rev 18002
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.
mengj [Fri, 28 Oct 2005 02:27:19 +0200] rev 18001
Added new functions to handle HOL goals and lemmas.
Added a funtion to send types and sorts information to ATP: they are clauses written to a separate file.
Removed several functions definitions, and combined them with those in other files.
mengj [Fri, 28 Oct 2005 02:25:57 +0200] rev 18000
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.
Also added function "repeat_RS" to the signature.
mengj [Fri, 28 Oct 2005 02:24:58 +0200] rev 17999
Added several functions to the signature.
Added two new functions, which are used by res_hol_clause.ML programs.
mengj [Fri, 28 Oct 2005 02:23:49 +0200] rev 17998
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.
paulson [Thu, 27 Oct 2005 18:25:33 +0200] rev 17997
sorted lemma lists
wenzelm [Thu, 27 Oct 2005 13:59:06 +0200] rev 17996
* HOL: alternative iff syntax;
wenzelm [Thu, 27 Oct 2005 13:54:43 +0200] rev 17995
consts: monomorphic;
wenzelm [Thu, 27 Oct 2005 13:54:42 +0200] rev 17994
removed inappropriate monomorphic test;
wenzelm [Thu, 27 Oct 2005 13:54:40 +0200] rev 17993
replaced Defs.monomorphic by Sign.monomorphic;
wenzelm [Thu, 27 Oct 2005 13:54:38 +0200] rev 17992
alternative iff syntax for equality on booleans, with print_mode 'iff';
haftmann [Thu, 27 Oct 2005 08:14:05 +0200] rev 17991
added module Pure/General/rat.ML
paulson [Wed, 26 Oct 2005 16:31:53 +0200] rev 17990
tidied away duplicate thm
wenzelm [Tue, 25 Oct 2005 18:38:21 +0200] rev 17989
EVERY;
wenzelm [Tue, 25 Oct 2005 18:18:59 +0200] rev 17988
traceIt: plain term;
wenzelm [Tue, 25 Oct 2005 18:18:58 +0200] rev 17987
val legacy = ref false;
wenzelm [Tue, 25 Oct 2005 18:18:57 +0200] rev 17986
prove_raw: cterms, explicit asms;
prove: Pattern.matches beta_norm;
wenzelm [Tue, 25 Oct 2005 18:18:49 +0200] rev 17985
avoid legacy goals;
wenzelm [Sat, 22 Oct 2005 01:22:10 +0200] rev 17984
legacy = ref true for the time being -- avoid volumious warnings;
wenzelm [Fri, 21 Oct 2005 18:20:29 +0200] rev 17983
tuned;
wenzelm [Fri, 21 Oct 2005 18:17:00 +0200] rev 17982
avoid OldGoals shortcuts;
wenzelm [Fri, 21 Oct 2005 18:16:57 +0200] rev 17981
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
* Internal goals: structure Goal.
wenzelm [Fri, 21 Oct 2005 18:15:00 +0200] rev 17980
Internal goals.
wenzelm [Fri, 21 Oct 2005 18:14:59 +0200] rev 17979
renamed triv_goal to goalI, rev_triv_goal to goalD;
wenzelm [Fri, 21 Oct 2005 18:14:58 +0200] rev 17978
tuned header;
wenzelm [Fri, 21 Oct 2005 18:14:57 +0200] rev 17977
Goal.norm_hhf_rule;
wenzelm [Fri, 21 Oct 2005 18:14:56 +0200] rev 17976
export add_binds_i;
invoke_case: AutoBind.no_facts;
Goal.init, Goal.conclude;
wenzelm [Fri, 21 Oct 2005 18:14:55 +0200] rev 17975
load_file: setmp OldGoals.legacy true;
wenzelm [Fri, 21 Oct 2005 18:14:54 +0200] rev 17974
improved check_result;
Goal.init, Goal.conclude;
wenzelm [Fri, 21 Oct 2005 18:14:53 +0200] rev 17973
Goal.prove_plain;