doc-src/Sledgehammer/sledgehammer.tex

 General or press the Emacs key sequence C-c C-a C-s.
 Either way, Sledgehammer produces the following output after a few seconds:
 
 \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
 the theory text. You can click the ``\textbf{sledgehammer} \textit{minimize}''
 command if you want to look for a shorter (and probably faster) proof. But here

 length of the Isar proofs can be controlled by setting
 \textit{isar\_shrink\_factor} (\S\ref{output-format}).
 \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}
 
 This sections answers frequently (and infrequently) asked questions about

 is usually stronger, but you need to have Z3 available to replay the proofs,
 trust the SMT solver, or use certificates. See the documentation in the
 \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}
 
 In some rare cases, Metis fails fairly quickly. This usually indicates that
 Sledgehammer found a type-incorrect proof. Sledgehammer erases some type