# HG changeset patch
# User blanchet
# Date 1324476268 -3600
# Node ID 87a446a6496db6a26bbe4ef7f32875372a65014b
# Parent  70b9d1e9fddcc12f1df25a19f1f4fb6e77223439
updated docs

diff -r 70b9d1e9fddc -r 87a446a6496d doc-src/Sledgehammer/sledgehammer.tex
--- 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}''}.