# HG changeset patch
# User blanchet
# Date 1315423881 -7200
# Node ID efa1f532508b739005fa386300d7aeaf55b1d367
# Parent  19b70980a1bb3976c2de58ce20a15d9ed6920faa
update Sledgehammer docs

diff -r 19b70980a1bb -r efa1f532508b doc-src/Sledgehammer/sledgehammer.tex
--- 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.