# HG changeset patch
# User blanchet
# Date 1338971705 -7200
# Node ID ebc75afed39a91d3ae0a70c6647f810517ca0475
# Parent  c84abbf3c5d879a58833d17522cd3cd4d50aa63a
updated docs

diff -r c84abbf3c5d8 -r ebc75afed39a doc-src/Sledgehammer/sledgehammer.tex
--- 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}