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.

--- 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")]];