--- a/src/HOL/Tools/ATP/atp_systems.ML Mon May 28 13:38:07 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon May 28 20:25:38 2012 +0200
@@ -327,7 +327,10 @@
(* LEO-II *)
-val leo2_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice)
+(* LEO-II supports definitions, but it performs significantly better on our
+ benchmarks when they are not used. *)
+val leo2_thf0 =
+ THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs)
val leo2_config : atp_config =
{exec = (["LEO2_HOME"], "leo"),
@@ -352,7 +355,8 @@
(* Satallax *)
-val satallax_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice)
+val satallax_thf0 =
+ THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
val satallax_config : atp_config =
{exec = (["SATALLAX_HOME"], "satallax"),
@@ -532,7 +536,8 @@
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
-val dummy_thf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
+val dummy_thf_format =
+ THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher"
val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)