# HG changeset patch
# User blanchet
# Date 1379709570 -7200
# Node ID a198ce71de119635cd0c56bad472b29429a08d6e
# Parent  be1874de8344b335c0db6dfb579eba76dc5b3257
took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired

diff -r be1874de8344 -r a198ce71de11 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Fri Sep 20 22:39:30 2013 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Fri Sep 20 22:39:30 2013 +0200
@@ -144,8 +144,8 @@
 Comments and bug reports concerning Sledgehammer or this manual should be
 directed to the author at \authoremail.
 
-\vskip2.5\smallskipamount
-
+%\vskip2.5\smallskipamount
+%
 %\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
 %suggesting several textual improvements.
 
@@ -292,20 +292,16 @@
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount]
 %
-Sledgehammer: ``\textit{remote\_waldmeister\/}'' on goal \\
-$[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount]
-%
 Sledgehammer: ``\textit{remote\_e\_sine\/}'' on goal \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms).
 \postw
 
-Sledgehammer ran E, E-SInE, SPASS, Vampire, Waldmeister, 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. Waldmeister is run only for unit equational problems,
-where the goal's conclusion is a (universally quantified) equation.
+Sledgehammer ran E, E-SInE, SPASS, Vampire, 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.
+Waldmeister is run only for unit equational problems, where the goal's
+conclusion is a (universally quantified) equation.
 
 For each successful prover, Sledgehammer gives a one-liner \textit{metis} or
 \textit{smt} method call. Rough timings are shown in parentheses, indicating how
@@ -338,7 +334,7 @@
 least \textit{safe} followed by \textit{simp\_all}. The SMT solvers provide
 arithmetic decision procedures, but the ATPs typically do not (or if they do,
 Sledgehammer does not use it yet). Apart from Waldmeister, they are not
-especially good at heavy rewriting, but because they regard equations as
+particularly good at heavy rewriting, but because they regard equations as
 undirected, they often prove theorems that require the reverse orientation of a
 \textit{simp} rule. Higher-order problems can be tackled, but the success rate
 is better for first-order problems. Hence, you may get better results if you
@@ -989,10 +985,10 @@
 \end{enum}
 
 By default, Sledgehammer runs a selection of CVC3, E, E-SInE, SPASS, Vampire,
-Yices, Z3, and (if appropriate) Waldmeister in parallel---either locally or
-remotely, depending on the number of processor cores available. (For historical
-reasons, the default value of this option can be overridden using the option
-``Sledgehammer: Provers'' in Proof General's ``Isabelle'' menu.)
+Yices, and Z3 in parallel---either locally or remotely, depending on the number
+of processor cores available. (For historical reasons, the default value of this
+option can be overridden using the option ``Sledgehammer: Provers'' in Proof
+General's ``Isabelle'' menu.)
 
 It is generally a good idea to run several provers in parallel. Running E,
 SPASS, and Vampire for 5~seconds yields a similar success rate to running the
diff -r be1874de8344 -r a198ce71de11 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Sep 20 22:39:30 2013 +0200
@@ -218,7 +218,7 @@
 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
    timeout, it makes sense to put E first. *)
 fun default_provers_param_value ctxt =
-  [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN]
+  [eN, spassN, vampireN, z3N, e_sineN, yicesN]
   |> map_filter (remotify_prover_if_not_installed ctxt)
   |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
                                   max_default_remote_threads)