author blanchet Thu, 19 May 2011 10:24:13 +0200 changeset 42846 dfed4dbe5596 parent 42845 94c69e441440 child 42847 06d3ce527d29
minor doc fixes
--- 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