--- a/doc-src/Sledgehammer/sledgehammer.tex Wed Jul 04 13:08:44 2012 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Jul 04 13:08:44 2012 +0200
@@ -1115,10 +1115,11 @@
\item[\labelitemi]
\textbf{%
-\textit{poly\_guards}@?, \textit{raw\_mono\_guards}@? (sound*):} \\
+\textit{poly\_guards}@, \textit{poly\_tags}@, \textit{raw\_mono\_guards}@, \\
+\textit{raw\_mono\_tags}@ (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\/}''}.
+\textit{metis} proof method, the `\hbox{@}' suffix is replaced by
+\hbox{``\textit{\_at\/}''}.
\item[\labelitemi] \textbf{\textit{poly\_args}?, \textit{raw\_mono\_args}? (unsound):} \\
Lighter versions of \textit{poly\_args} and \textit{raw\_mono\_args}.