added Zipperposition to sledgehammer's default provers
authordesharna
Tue, 28 Sep 2021 10:38:36 +0200
changeset 74737 3301c0d8b560
parent 74736 ac90d6c6c149
child 74738 d8dc8fdc46fc
added Zipperposition to sledgehammer's default provers
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Sep 27 20:45:26 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Tue Sep 28 10:38:36 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, z3N, eN, spassN, veritN]
+  [cvc4N, vampireN, z3N, eN, spassN, veritN, zipperpositionN]
   |> 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))