--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Apr 05 10:37:21 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Apr 05 10:47:36 2011 +0200
@@ -564,19 +564,16 @@
\item[$\bullet$] \textbf{\textit{tags}:} Each term (and subterm) is tagged with
its type.
-% NOT YET IMPLEMENTED:
-%\item[$\bullet$] \textbf{\textit{preds}:} Types are represented by predicates.
-
\item[$\bullet$] \textbf{\textit{mangled}:} Types are mangled in constant names.
This value is available only if \textit{monomorphize} is enabled and
-\textit{full\_types} is enabled.
+\textit{full\_types} is disabled.
\item[$\bullet$] \textbf{\textit{const\_args}:} Constants are annotated with
-their type parameters, which are passed as extra arguments. This value is not
-available if \textit{full\_types} is enabled.
+their type parameters, which are passed as extra arguments. This value is
+ignored if \textit{full\_types} is enabled.
\item[$\bullet$] \textbf{\textit{none}:} No type information is supplied to the
-ATP.
+ATP. This value is ignored if \textit{full\_types} is enabled.
\item[$\bullet$] \textbf{\textit{smart}:} This is the same as
\textit{tags} if \textit{full\_types} is enabled; otherwise, this is the