# HG changeset patch
# User blanchet
# Date 1305793453 -7200
# Node ID dfed4dbe559608e8168e74d1220cc52af865b818
# Parent  94c69e4414400645cf7253d976339b26fb89a3bb
minor doc fixes

diff -r 94c69e441440 -r dfed4dbe5596 doc-src/Sledgehammer/sledgehammer.tex
--- 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