--- a/src/HOL/Tools/res_atp_methods.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/res_atp_methods.ML Thu Jan 19 21:22:08 2006 +0100
@@ -46,16 +46,13 @@
val eproverH_tac = res_atp_tac eprover_oracle ResAtpSetup.Hol (!eprover_time);
-val ResAtps_setup = [Method.add_methods
- [("vampireF", ResAtpSetup.atp_method vampireF_tac, "A Vampire method for FOL problems"),
- ("eproverF", ResAtpSetup.atp_method eproverF_tac, "A E prover method for FOL problems"),
- ("vampireH",ResAtpSetup.atp_method vampireH_tac, "A Vampire method for HOL problems"),
- ("eproverH",ResAtpSetup.atp_method eproverH_tac,"A E prover method for HOL problems"),
- ("eprover",ResAtpSetup.atp_method eprover_tac,"A E prover method for FOL and HOL problems"),
- ("vampire",ResAtpSetup.atp_method vampire_tac,"A Vampire method for FOL and HOL problems")
-]];
-
-
-
+val ResAtps_setup =
+ Method.add_methods
+ [("vampireF", ResAtpSetup.atp_method vampireF_tac, "Vampire for FOL problems"),
+ ("eproverF", ResAtpSetup.atp_method eproverF_tac, "E prover for FOL problems"),
+ ("vampireH", ResAtpSetup.atp_method vampireH_tac, "Vampire for HOL problems"),
+ ("eproverH", ResAtpSetup.atp_method eproverH_tac, "E prover for HOL problems"),
+ ("eprover", ResAtpSetup.atp_method eprover_tac, "E prover for FOL and HOL problems"),
+ ("vampire", ResAtpSetup.atp_method vampire_tac, "Vampire for FOL and HOL problems")];
end