--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed May 25 14:39:46 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri May 27 13:46:40 2022 +0200
@@ -41,7 +41,9 @@
val refresh_systems_on_tptp : unit -> unit
val local_atps : string list
val remote_atps : string list
- val atps : string list
+ val dummy_atps : string list
+ val non_dummy_atps : string list
+ val all_atps : string list
end;
structure Sledgehammer_ATP_Systems : SLEDGEHAMMER_ATP_SYSTEMS =
@@ -568,13 +570,18 @@
[agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, zipperposition]
val remote_atps =
[remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3,
- remote_waldmeister, remote_zipperposition, dummy_fof, dummy_tfx, dummy_thf, dummy_thf_reduced]
-val atps = local_atps @ remote_atps
+ remote_waldmeister, remote_zipperposition]
+val dummy_atps =
+ [dummy_fof, dummy_tfx, dummy_thf, dummy_thf_reduced]
+val non_dummy_atps = local_atps @ remote_atps
+val all_atps = non_dummy_atps @ dummy_atps
-val _ = Theory.setup (fold add_atp atps)
+val _ = Theory.setup (fold add_atp all_atps)
val local_atps = map fst local_atps
val remote_atps = map fst remote_atps
-val atps = map fst atps
+val dummy_atps = map fst dummy_atps
+val non_dummy_atps = map fst non_dummy_atps
+val all_atps = map fst all_atps
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed May 25 14:39:46 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri May 27 13:46:40 2022 +0200
@@ -162,7 +162,8 @@
(* The first ATP of the list is used by Auto Sledgehammer. *)
fun default_provers_param_value ctxt =
- filter (is_prover_installed ctxt) (smts ctxt @ atps) \<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close>
+ \<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close>
+ filter (is_prover_installed ctxt) (smts ctxt @ non_dummy_atps)
|> implode_param
fun set_default_raw_param param thy =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed May 25 14:39:46 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri May 27 13:46:40 2022 +0200
@@ -127,7 +127,7 @@
| induction_rules_of_string "instantiate" = SOME Instantiate
| induction_rules_of_string _ = NONE
-val is_atp = member (op =) atps
+val is_atp = member (op =) all_atps
type params =
{debug : bool,