--- a/src/HOL/Tools/res_atp.ML Fri Sep 02 17:55:24 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Fri Sep 02 21:29:33 2005 +0200
@@ -189,13 +189,22 @@
optionline, clasimpfile, axfile, hypsfile, probfile)] @
(make_atp_list xs sign (n+1)))
end
- else
+ else if !vampire
+ then
let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
in
([("vampire", thmstr, goalstring, vampire, "-t 60%-m 100000",
clasimpfile, axfile, hypsfile, probfile)] @
(make_atp_list xs sign (n+1)))
end
+ else
+ let val Eprover = ResLib.helper_path "E_HOME" "eproof"
+ in
+ ([("E", thmstr, goalstring, Eprover, "--tptp-in -l5",
+ clasimpfile, axfile, hypsfile, probfile)] @
+ (make_atp_list xs sign (n+1)))
+ end
+
end
val atp_list = make_atp_list (ListPair.zip (thms, sg_terms)) sign 1