--- a/doc-src/Sledgehammer/sledgehammer.tex Fri May 27 10:30:08 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Fri May 27 10:30:08 2011 +0200
@@ -249,33 +249,33 @@
\slshape
Sledgehammer: ``\textit{e}'' on goal: \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this command: \textbf{by} (\textit{metis last\_ConsL}). \\
+Try this: \textbf{by} (\textit{metis last\_ConsL}). \\
To minimize: \textbf{sledgehammer} \textit{min} [\textit{e}] (\textit{last\_ConsL}). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{vampire}'' on goal: \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this command: \textbf{by} (\textit{metis hd.simps}). \\
+Try this: \textbf{by} (\textit{metis hd.simps}). \\
To minimize: \textbf{sledgehammer} \textit{min} [\textit{vampire}] (\textit{hd.simps}). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{spass}'' on goal: \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this command: \textbf{by} (\textit{metis list.inject}). \\
+Try this: \textbf{by} (\textit{metis list.inject}). \\
To minimize: \textbf{sledgehammer} \textit{min} [\textit{spass}]~(\textit{list.inject}). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{remote\_waldmeister}'' on goal: \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this command: \textbf{by} (\textit{metis hd.simps insert\_Nil}). \\
+Try this: \textbf{by} (\textit{metis hd.simps insert\_Nil}). \\
To minimize: \textbf{sledgehammer} \textit{min} [\textit{remote\_waldmeister}] \\
\phantom{To minimize: \textbf{sledgehammer}~}(\textit{hd.simps insert\_Nil}). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{remote\_sine\_e}'' on goal: \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this command: \textbf{by} (\textit{metis hd.simps}). \\
+Try this: \textbf{by} (\textit{metis hd.simps}). \\
To minimize: \textbf{sledgehammer} \textit{min} [\textit{remote\_sine\_e}]~(\textit{hd.simps}). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{remote\_z3}'' on goal: \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this command: \textbf{by} (\textit{metis hd.simps}). \\
+Try this: \textbf{by} (\textit{metis hd.simps}). \\
To minimize: \textbf{sledgehammer} \textit{min} [\textit{remote\_z3}]~(\textit{hd.simps}).
\postw