# HG changeset patch
# User blanchet
# Date 1306485007 -7200
# Node ID b48aa3492f0ba19de6ac9525552f47fcef5791c9
# Parent  ff631c45797e73862b5f5d27a7b32eed37757f8a
minor doc adjustments

diff -r ff631c45797e -r b48aa3492f0b doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Fri May 27 10:30:07 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri May 27 10:30:07 2011 +0200
@@ -250,39 +250,34 @@
 Sledgehammer: ``\textit{e}'' for subgoal 1: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 Try this command: \textbf{by} (\textit{metis last\_ConsL}). \\
-To minimize the number of lemmas, try this: \\
-\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{e}] (\textit{last\_ConsL}). \\[3\smallskipamount]
+To minimize: \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{e}] (\textit{last\_ConsL}). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{vampire}'' for subgoal 1: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 Try this command: \textbf{by} (\textit{metis hd.simps}). \\
-To minimize the number of lemmas, try this: \\
-\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{vampire}] (\textit{hd.simps}). \\[3\smallskipamount]
+To minimize: \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{vampire}] (\textit{hd.simps}). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{spass}'' for subgoal 1: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 Try this command: \textbf{by} (\textit{metis list.inject}). \\
-To minimize the number of lemmas, try this: \\
-\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{spass}]~(\textit{list.inject}). \\[3\smallskipamount]
+To minimize: \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{spass}]~(\textit{list.inject}). \\[3\smallskipamount]
 %
 %Sledgehammer: ``\textit{remote\_waldmeister}'' for subgoal 1: \\
 %$[a] = [b] \,\Longrightarrow\, a = b$ \\
 %Try this command: \textbf{by} (\textit{metis hd.simps insert\_Nil}). \\
-%To minimize the number of lemmas, try this: \\
-%\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_waldmeister}] \\
+%To minimize: \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_waldmeister}] \\
 %\phantom{\textbf{sledgehammer}~}(\textit{hd.simps insert\_Nil}). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{remote\_sine\_e}'' for subgoal 1: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 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}). \\[3\smallskipamount]
+To minimize: \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}] \\
+\phantom{To minimize: }(\textit{hd.simps}). \\[3\smallskipamount]
 %
 Sledgehammer: ``\textit{remote\_z3}'' for subgoal 1: \\
 $[a] = [b] \,\Longrightarrow\, a = b$ \\
 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\_z3}]~(\textit{hd.simps}).
+To minimize: \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_z3}]~(\textit{hd.simps}).
 \postw
 
 Sledgehammer ran E, SInE-E, SPASS, Vampire, %Waldmeister,
@@ -356,8 +351,8 @@
 \item[$\bullet$] \textbf{\textit{full\_types}} (\S\ref{problem-encoding})
 specifies whether type-sound encodings should be used. By default, Sledgehammer
 employs a mixture of type-sound and type-unsound encodings, occasionally
-yielding unsound ATP proofs. (SMT solver proofs should always be sound, although
-we occasionally find soundness bugs in the solvers.)
+yielding unsound ATP proofs. In contrast, SMT solver proofs should always be
+sound.
 
 \item[$\bullet$] \textbf{\textit{max\_relevant}} (\S\ref{relevance-filter})
 specifies the maximum number of facts that should be passed to the provers. By
@@ -529,8 +524,8 @@
 If you see the warning
 
 \prew
-\textsl
-Metis: Falling back on ``\textit{metisFT}''.
+\slshape
+Metis: Falling back on ``\textit{metisFT\/}''.
 \postw
 
 in a successful Metis proof, you can advantageously replace the \textit{metis}