src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Apr 07 08:39:10 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Apr 07 09:13:10 2025 +0200
@@ -170,9 +170,13 @@
 
 (* The first ATP of the list is used by Auto Sledgehammer. *)
 fun default_provers_param_value ctxt =
-  \<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close>
-  filter (is_prover_installed ctxt) (smt_solvers ctxt @ local_atps)
-  |> implode_param
+  let
+    val try0_provers = Try0.get_all_proof_method_names ()
+    \<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close>
+    val installed_provers = filter (is_prover_installed ctxt) (smt_solvers ctxt @ local_atps)
+  in
+    implode_param (installed_provers @ try0_provers)
+  end
 
 fun set_default_raw_param param thy =
   let val ctxt = Proof_Context.init_global thy in