# HG changeset patch # User blanchet # Date 1406286950 -7200 # Node ID 9bfa4cb2fee6f5feecb98f47f39ba1c90ed83d84 # Parent d53b1f876afbbe9c4da2d66570b1b7196e965eca reordered provers diff -r d53b1f876afb -r 9bfa4cb2fee6 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Jul 25 12:22:18 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Jul 25 13:15:50 2014 +0200 @@ -203,10 +203,9 @@ if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name else remotify_prover_if_supported_and_not_already_remote ctxt name -(* The first ATP of the list is used by Auto Sledgehammer. Because of the low - timeout, it makes sense to put E first. *) +(* The first ATP of the list is used by Auto Sledgehammer. *) fun default_provers_param_value mode ctxt = - [eN, spassN, z3N, e_sineN, vampireN] + [eN, spassN, z3N, vampireN, e_sineN] |> 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_value () - (if mode = Try then 1 else 0))