# HG changeset patch
# User blanchet
# Date 1435228903 -7200
# Node ID a9b71c82647b103076bac6614cc0d465a0d28ddf
# Parent  19c277ea65aeea5a5851bfd70520eda19b812901
put E before (typically remote, hence less reliable) Vampire

diff -r 19c277ea65ae -r a9b71c82647b src/Doc/Sledgehammer/document/root.tex
--- 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.
 
diff -r 19c277ea65ae -r a9b71c82647b src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- 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))