# HG changeset patch
# User mengj
# Date 1130459300 -7200
# Node ID 35ec4681d38f3062f3ef41acf3ce6fc44ef6f5d5
# Parent  6ca14bec7cd591b40de1418caedd35bbb76542b7
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.

diff -r 6ca14bec7cd5 -r 35ec4681d38f src/HOL/Tools/res_atp_methods.ML
--- a/src/HOL/Tools/res_atp_methods.ML	Fri Oct 28 02:27:19 2005 +0200
+++ b/src/HOL/Tools/res_atp_methods.ML	Fri Oct 28 02:28:20 2005 +0200
@@ -25,24 +25,28 @@
 
 
 (* convert the negated 1st subgoal into CNF, write to files and call an ATP oracle *)
-fun res_atp_tac res_atp_oracle timeLimit ctxt files tfrees n thm =
+fun res_atp_tac res_atp_oracle tptp_form make_nnf timeLimit ctxt files tfrees n thm =
     SELECT_GOAL
 	((EVERY1 [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac, 
 		  METAHYPS(fn negs =>
 			      HEADGOAL(Tactic.rtac 
 					   (res_atp_oracle (ProofContext.theory_of ctxt) 
-							   ((ResAtpSetup.tptp_form (make_clauses (map make_nnf negs)) n tfrees)::files, timeLimit))))]) handle Fail _ => no_tac) n thm;
+							   ((tptp_form (make_clauses (map make_nnf negs)) n tfrees)::files, timeLimit))))]) handle Fail _ => no_tac) n thm;
 
+(* vampire and eprover tactics *)
+val vampireF_tac = res_atp_tac vampire_oracle ResAtpSetup.tptp_form make_nnf (!vampire_time);
 
-(* vampire_tac and eprover_tac *)
-val vampire_tac = res_atp_tac vampire_oracle (!vampire_time);
+val vampireH_tac = res_atp_tac vampire_oracle ResAtpSetup.tptp_formH make_nnf1 (!vampire_time);
 
-val eprover_tac = res_atp_tac eprover_oracle (!eprover_time);
+val eproverF_tac = res_atp_tac eprover_oracle ResAtpSetup.tptp_form make_nnf (!eprover_time);
 
+val eproverH_tac = res_atp_tac eprover_oracle ResAtpSetup.tptp_formH make_nnf1 (!eprover_time);
 
 val ResAtps_setup = [Method.add_methods 
-		 [("vampire", ResAtpSetup.atp_method vampire_tac, "A Vampire method"),
-		   ("eprover", ResAtpSetup.atp_method eprover_tac, "A E prover method")]];
+		 [("vampireF", ResAtpSetup.atp_method_F vampireF_tac, "A Vampire method for FOL problems"),
+		   ("eproverF", ResAtpSetup.atp_method_F eproverF_tac, "A E prover method for FOL problems"),
+			("vampireH",ResAtpSetup.atp_method_H vampireH_tac, "A Vampire method for HOL problems"),
+				("eproverH",ResAtpSetup.atp_method_H eproverH_tac,"A E prover method for HOL problems")]];