# HG changeset patch
# User blanchet
# Date 1338971705 -7200
# Node ID 433787f8145e3bd9de8ea82f901821cfdf582563
# Parent  fcb2292aa2604fea0e2f9725766d29e9bda9655b
updated docs

diff -r fcb2292aa260 -r 433787f8145e 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
@@ -1037,12 +1037,12 @@
 below) is enabled.
 
 \begin{enum}
-\item[\labelitemi] \textbf{\textit{erased} (very unsound):} No type information is
+\item[\labelitemi] \textbf{\textit{erased} (unsound):} No type information is
 supplied to the ATP, not even to resolve overloading. Types are simply erased.
 
 \item[\labelitemi] \textbf{\textit{poly\_guards} (sound):} Types are encoded using
 a predicate \const{g}$(\tau, t)$ that guards bound
-variables. Constants are annotated with their types, supplied as additional
+variables. Constants are annotated with their types, supplied as extra
 arguments, to resolve overloading.
 
 \item[\labelitemi] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
@@ -1051,7 +1051,7 @@
 \item[\labelitemi] \textbf{\textit{poly\_args} (unsound):}
 Like for \textit{poly\_guards} constants are annotated with their types to
 resolve overloading, but otherwise no type information is encoded. This
-coincides with the default encoding used by the \textit{metis} command.
+is the default encoding used by the \textit{metis} command.
 
 \item[\labelitemi]
 \textbf{%
@@ -1120,38 +1120,6 @@
 \textit{metis} proof method, the `\hbox{@?}' suffix is replaced by
 \hbox{``\textit{\_at\_query\/}''}.
 
-\item[\labelitemi]
-\textbf{%
-\textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\
-\textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\
-\textit{mono\_native}!, \textit{mono\_native\_higher}! (mildly unsound):} \\
-The type encodings \textit{poly\_guards}, \textit{poly\_tags},
-\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
-\textit{mono\_tags}, \textit{mono\_native}, and \textit{mono\_native\_higher}
-also admit a mildly unsound (but very efficient) variant identified by an
-exclamation mark (`\hbox{!}') that detects and erases erases all types except
-those that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_native}
-and \textit{mono\_native\_higher}, the types are not actually erased but rather
-replaced by a shared uniform type of individuals.) As argument to the
-\textit{metis} proof method, the exclamation mark is replaced by the suffix
-\hbox{``\textit{\_bang\/}''}.
-
-\item[\labelitemi]
-\textbf{%
-\textit{poly\_guards}!!, \textit{poly\_tags}!!, \textit{raw\_mono\_guards}!!, \\
-\textit{raw\_mono\_tags}!!, \textit{mono\_guards}!!, \textit{mono\_tags}!! \\
-(mildly unsound):} \\
-Even lighter versions of the `\hbox{!}' encodings. As argument to the
-\textit{metis} proof method, the `\hbox{!!}' suffix is replaced by
-\hbox{``\textit{\_bang\_bang\/}''}.
-
-\item[\labelitemi]
-\textbf{%
-\textit{poly\_guards}@!, \textit{raw\_mono\_guards}@! (mildly unsound):} \\
-Alternative versions of the `\hbox{!!}' encodings. As argument to the
-\textit{metis} proof method, the `\hbox{@!}' suffix is replaced by
-\hbox{``\textit{\_at\_bang\/}''}.
-
 \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}