--- a/doc-src/Sledgehammer/sledgehammer.tex Wed Dec 21 15:04:28 2011 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Dec 21 15:04:28 2011 +0100
@@ -1061,8 +1061,7 @@
\item[\labelitemi]
\textbf{%
-\textit{poly\_guards}@?, \textit{poly\_tags}@?, \textit{raw\_mono\_guards}@?, \\
-\textit{raw\_mono\_tags}@? (quasi-sound):} \\
+\textit{poly\_guards}@?, \textit{raw\_mono\_guards}@? (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}''}.
@@ -1094,8 +1093,7 @@
\item[\labelitemi]
\textbf{%
-\textit{poly\_guards}@!, \textit{poly\_tags}@!, \textit{raw\_mono\_guards}@!, \\
-\textit{raw\_mono\_tags}@! (mildly unsound):} \\
+\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}''}.