Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
formal comment concerning 83d2208252d1 vs. d8dc8fdc46fc;
authorwenzelm
Mon, 04 Oct 2021 14:07:15 +0200
changeset 74436 4e30de0b4dd6
parent 74435 4bb1251043cd
child 74437 e1b5bf983de3
formal comment concerning 83d2208252d1 vs. d8dc8fdc46fc;
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML file | annotate | diff | comparison | revisions 
--- 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))
isabelle