# HG changeset patch
# User blanchet
# Date 1341400124 -7200
# Node ID 7c48419c89c5b59b408c96e23b8bf3c45695d459
# Parent  6c0ac78154669c681c3d4bab58448e606e072a1f
update docs

diff -r 6c0ac7815466 -r 7c48419c89c5 doc-src/Sledgehammer/sledgehammer.tex
--- 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}.