# HG changeset patch
# User wenzelm
# Date 1633349235 -7200
# Node ID 4e30de0b4dd6bcdf2cd83648fbc465dd839fffcc
# Parent  4bb1251043cd3f403490921c7f41a684cf4b5cfd
formal comment concerning 83d2208252d1 vs. d8dc8fdc46fc;

diff -r 4bb1251043cd -r 4e30de0b4dd6 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Oct 04 14:02:11 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Oct 04 14:07:15 2021 +0200
@@ -177,7 +177,7 @@
 
 (* The first ATP of the list is used by Auto Sledgehammer. *)
 fun default_provers_param_value mode ctxt =
-  [cvc4N, vampireN, veritN, eN, spassN, z3N, zipperpositionN]
+  [cvc4N, vampireN, veritN, eN, spassN, z3N, zipperpositionN] \<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close>
   |> map_filter (remotify_prover_if_not_installed ctxt)
   (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
   |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0))