# HG changeset patch
# User blanchet
# Date 1306485007 -7200
# Node ID a14cf580a5a54d85f4d43cbe40d127817b2aa16e
# Parent  f58bab6be6a9747048095111d8adc9c5f81b938b
readded Waldmeister as default to the documentation and other minor changes

diff -r f58bab6be6a9 -r a14cf580a5a5 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Fri May 27 10:30:07 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri May 27 10:30:07 2011 +0200
@@ -247,45 +247,43 @@
 
 \prew
 \slshape
-Sledgehammer: ``\textit{e}'' for subgoal 1: \\
+Sledgehammer: ``\textit{e}'' on goal: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 Try this command: \textbf{by} (\textit{metis last\_ConsL}). \\
 To minimize: \textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{e}] (\textit{last\_ConsL}). \\[3\smallskipamount]
 %
-Sledgehammer: ``\textit{vampire}'' for subgoal 1: \\
+Sledgehammer: ``\textit{vampire}'' on goal: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 Try this command: \textbf{by} (\textit{metis hd.simps}). \\
 To minimize: \textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{vampire}] (\textit{hd.simps}). \\[3\smallskipamount]
 %
-Sledgehammer: ``\textit{spass}'' for subgoal 1: \\
+Sledgehammer: ``\textit{spass}'' on goal: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 Try this command: \textbf{by} (\textit{metis list.inject}). \\
 To minimize: \textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{spass}]~(\textit{list.inject}). \\[3\smallskipamount]
 %
-%Sledgehammer: ``\textit{remote\_waldmeister}'' for subgoal 1: \\
-%$[a] = [b] \,\Longrightarrow\, a = b$ \\
-%Try this command: \textbf{by} (\textit{metis hd.simps insert\_Nil}). \\
-%To minimize: \textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{remote\_waldmeister}] \\
-%\phantom{\textbf{sledgehammer}~}(\textit{hd.simps insert\_Nil}). \\[3\smallskipamount]
+Sledgehammer: ``\textit{remote\_waldmeister}'' on goal: \\
+$[a] = [b] \,\Longrightarrow\, a = b$ \\
+Try this command: \textbf{by} (\textit{metis hd.simps insert\_Nil}). \\
+To minimize: \textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{remote\_waldmeister}] \\
+\phantom{To minimize: \textbf{sledgehammer}~}(\textit{hd.simps insert\_Nil}). \\[3\smallskipamount]
 %
-Sledgehammer: ``\textit{remote\_sine\_e}'' for subgoal 1: \\
+Sledgehammer: ``\textit{remote\_sine\_e}'' on goal: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 Try this command: \textbf{by} (\textit{metis hd.simps}). \\
 To minimize: \textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}). \\[3\smallskipamount]
 %
-Sledgehammer: ``\textit{remote\_z3}'' for subgoal 1: \\
+Sledgehammer: ``\textit{remote\_z3}'' on goal: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 Try this command: \textbf{by} (\textit{metis hd.simps}). \\
 To minimize: \textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{remote\_z3}]~(\textit{hd.simps}).
 \postw
 
-Sledgehammer ran E, SInE-E, SPASS, Vampire, %Waldmeister,
-and Z3 in parallel.
+Sledgehammer ran E, SInE-E, 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.
+\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 proof that uses the
 \textit{metis} or \textit{smt} method. You can click the proof to insert it into
@@ -366,11 +364,11 @@
 \end{enum}
 
 Options can be set globally using \textbf{sledgehammer\_params}
-(\S\ref{command-syntax}). Fact selection can be influenced by specifying
-``$(\textit{add}{:}~\textit{my\_facts})$'' after the \textbf{sledgehammer}
-call to ensure that certain facts are included, or simply
-``$(\textit{my\_facts})$'' to force Sledgehammer to run only with
-$\textit{my\_facts}$.
+(\S\ref{command-syntax}). The command also prints the list of all available
+options with their current value. Fact selection can be influenced by specifying
+``$(\textit{add}{:}~\textit{my\_facts})$'' after the \textbf{sledgehammer} call
+to ensure that certain facts are included, or simply ``$(\textit{my\_facts})$''
+to force Sledgehammer to run only with $\textit{my\_facts}$.
 
 \section{Frequently Asked Questions}
 \label{frequently-asked-questions}
@@ -397,7 +395,7 @@
 \emph{SMT} theory (\texttt{\$ISABELLE\_HOME/src/HOL/SMT.thy}) for details.
 
 \item[$\bullet$] Try the \textit{blast} or \textit{auto} proof methods, passing
-facts via \textbf{unfolding}, \textbf{using}, \textit{intro}{:},
+the necessary facts via \textbf{unfolding}, \textbf{using}, \textit{intro}{:},
 \textit{elim}{:}, \textit{dest}{:}, or \textit{simp}{:}, as appropriate.
 \end{enum}