--- a/doc-src/Sledgehammer/sledgehammer.tex Wed Jun 06 10:35:05 2012 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Jun 06 10:35:05 2012 +0200
@@ -1030,9 +1030,9 @@
\opdefault{type\_enc}{string}{smart}
Specifies the type encoding to use in ATP problems. Some of the type encodings
are unsound, meaning that they can give rise to spurious proofs
-(unreconstructible using \textit{metis}). The supported type encodings are
+(unreconstructible using \textit{metis}). The type encodings are
listed below, with an indication of their soundness in parentheses.
-An asterisk (*) means that the encoding is slightly incomplete for
+An asterisk (*) indicates that the encoding is slightly incomplete for
reconstruction with \textit{metis}, unless the \emph{strict} option (described
below) is enabled.
@@ -1120,6 +1120,9 @@
\textit{metis} proof method, the `\hbox{@?}' suffix is replaced by
\hbox{``\textit{\_at\_query\/}''}.
+\item[\labelitemi] \textbf{\textit{poly\_args}?, \textit{raw\_mono\_args}? (unsound):} \\
+Lighter versions of \textit{poly\_args} and \textit{raw\_mono\_args}.
+
\item[\labelitemi] \textbf{\textit{smart}:} The actual encoding used depends on
the ATP and should be the most efficient sound encoding for that ATP.
\end{enum}