--- 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}