--- a/doc-src/Sledgehammer/sledgehammer.tex Thu May 19 10:24:13 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Thu May 19 10:24:13 2011 +0200
@@ -255,19 +255,19 @@
%
Sledgehammer: ``\textit{vampire}'' for subgoal 1: \\
$([a] = [b]) = (a = b)$ \\
-Try this command: \textbf{by} (\textit{metis eq\_commute last\_snoc}) \\
+Try this command: \textbf{by} (\textit{metis eq\_commute last\_snoc}). \\
To minimize the number of lemmas, try this: \\
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{vampire}]~(\textit{eq\_commute last\_snoc}). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{remote\_sine\_e}'' for subgoal 1: \\
$([a] = [b]) = (a = b)$ \\
-Try this command: \textbf{by} (\textit{metis hd.simps}) \\
+Try this command: \textbf{by} (\textit{metis hd.simps}). \\
To minimize the number of lemmas, try this: \\
-\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}).
+\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}). \\[3\smallskipamount]
%
Sledgehammer: ``\textit{remote\_z3}'' for subgoal 1: \\
$([a] = [b]) = (a = b)$ \\
-Try this command: \textbf{by} (\textit{metis hd.simps}) \\
+Try this command: \textbf{by} (\textit{metis hd.simps}). \\
To minimize the number of lemmas, try this: \\
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}).
\postw