# HG changeset patch
# User blanchet
# Date 1310649277 -7200
# Node ID 86cdb898f251fb290d35e4f46d62c0efce24be9a
# Parent  048619bb1dc3e269632997ea978d2767edd70864
clarify fine soundness point

diff -r 048619bb1dc3 -r 86cdb898f251 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Thu Jul 14 15:14:37 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu Jul 14 15:14:37 2011 +0200
@@ -980,8 +980,9 @@
 
 \opfalse{sound}{unsound}
 Specifies whether Sledgehammer should run in its fully sound mode. In that mode,
-quasi-sound type encodings are made fully sound, at the cost of some (usually
-needless) clutter.
+quasi-sound type encodings (which are the default) are made fully sound, at the
+cost of some clutter in the generated problems. This option is ignored if
+\textit{type\_enc} is explicitly set to an unsound encoding.
 \end{enum}
 
 \subsection{Relevance Filter}