--- 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}