--- 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
@@ -247,33 +247,33 @@
\prew
\slshape
-Sledgehammer: ``\textit{e}'' on goal: \\
+Sledgehammer: ``\textit{e}'' on goal \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
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: \\
+Sledgehammer: ``\textit{vampire}'' on goal \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
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: \\
+Sledgehammer: ``\textit{spass}'' on goal \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
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: \\
+Sledgehammer: ``\textit{remote\_waldmeister}'' on goal \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
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: \\
+Sledgehammer: ``\textit{remote\_sine\_e}'' on goal \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
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: \\
+Sledgehammer: ``\textit{remote\_z3}'' on goal \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
Try this: \textbf{by} (\textit{metis hd.simps}). \\
To minimize: \textbf{sledgehammer} \textit{min} [\textit{remote\_z3}]~(\textit{hd.simps}).