# HG changeset patch
# User blanchet
# Date 1306485008 -7200
# Node ID 31182f0ec04d07038290b745089ca0a141d345c1
# Parent  18259246abb5a317419e01460fcfd8d5a483288a
minor update

diff -r 18259246abb5 -r 31182f0ec04d doc-src/Sledgehammer/sledgehammer.tex
--- 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}).