--- a/src/Doc/Sledgehammer/document/root.tex Wed Jun 24 23:03:55 2015 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Jun 25 12:41:43 2015 +0200
@@ -266,14 +266,14 @@
Sledgehammer: ``\textit{z3\/}'' \\
Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \\[3\smallskipamount]
%
-Sledgehammer: ``\textit{remote\_vampire\/}'' \\
-Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount]
-%
Sledgehammer: ``\textit{spass\/}'' \\
Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount]
+%
+Sledgehammer: ``\textit{e\/}'' \\
+Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount]
\postw
-Sledgehammer ran CVC4, SPASS, Vampire, and Z3 in parallel. Depending on which
+Sledgehammer ran CVC4, E, SPASS, and Z3 in parallel. Depending on which
provers are installed and how many processor cores are available, some of the
provers might be missing or present with a \textit{remote\_} prefix.
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Jun 24 23:03:55 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Jun 25 12:41:43 2015 +0200
@@ -181,7 +181,7 @@
(* The first ATP of the list is used by Auto Sledgehammer. *)
fun default_provers_param_value mode ctxt =
- [cvc4N, vampireN, z3N, spassN, eN, veritN, e_sineN]
+ [cvc4N, z3N, spassN, eN, vampireN, veritN, 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))