--- a/doc-src/Sledgehammer/sledgehammer.tex Wed Sep 07 21:31:21 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Sep 07 21:31:21 2011 +0200
@@ -942,19 +942,29 @@
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
\textit{mono\_tags}, and \textit{mono\_simple} are fully
typed and sound. For each of these, Sledgehammer also provides a lighter,
-virtually sound variant identified by a question mark (`{?}')\ that detects and
-erases monotonic types, notably infinite types. (For \textit{mono\_simple}, 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 question mark
-is replaced by a \hbox{``\textit{\_query}''} suffix. If the \emph{sound} option
-is enabled, these encodings are fully sound.
+virtually sound variant identified by a question mark (`\hbox{?}')\ that detects
+and erases monotonic types, notably infinite types. (For \textit{mono\_simple},
+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 question
+mark is replaced by a \hbox{``\textit{\_query}''} suffix. If the \emph{sound}
+option is enabled, these encodings are fully sound.
\item[$\bullet$]
\textbf{%
\textit{poly\_guards}??, \textit{poly\_tags}??, \textit{raw\_mono\_guards}??, \\
\textit{raw\_mono\_tags}??, \textit{mono\_guards}??, \textit{mono\_tags}?? \\
(quasi-sound):} \\
-Even lighter versions of the `{?}' encodings.
+Even lighter versions of the `\hbox{?}' encodings. As argument to the
+\textit{metis} proof method, the `\hbox{??}' suffix is replaced by
+\hbox{``\textit{\_query\_query}''}.
+
+\item[$\bullet$]
+\textbf{%
+\textit{poly\_guards}@?, \textit{poly\_tags}@?, \textit{raw\_mono\_guards}@?, \\
+\textit{raw\_mono\_tags}@? (quasi-sound):} \\
+Alternative versions of the `\hbox{??}' encodings. As argument to the
+\textit{metis} proof method, the `\hbox{@?}' suffix is replaced by
+\hbox{``\textit{\_at\_query}''}.
\item[$\bullet$]
\textbf{%
@@ -965,9 +975,9 @@
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
\textit{mono\_tags}, \textit{mono\_simple}, and \textit{mono\_simple\_higher}
also admit a mildly unsound (but very efficient) variant identified by an
-exclamation mark (`{!}') that detects and erases erases all types except those
-that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_simple} and
-\textit{mono\_simple\_higher}, the types are not actually erased but rather
+exclamation mark (`\hbox{!}') that detects and erases erases all types except
+those that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_simple}
+and \textit{mono\_simple\_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}''}.
@@ -977,7 +987,17 @@
\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 `{!}' encodings.
+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[$\bullet$]
+\textbf{%
+\textit{poly\_guards}@!, \textit{poly\_tags}@!, \textit{raw\_mono\_guards}@!, \\
+\textit{raw\_mono\_tags}@! (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[$\bullet$] \textbf{\textit{smart}:} The actual encoding used depends on
the ATP and should be the most efficient virtually sound encoding for that ATP.