1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Wed Dec 21 15:04:28 2011 +0100
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed Dec 21 15:04:28 2011 +0100
     1.3 @@ -1061,8 +1061,7 @@
     1.4  
     1.5  \item[\labelitemi]
     1.6  \textbf{%
     1.7 -\textit{poly\_guards}@?, \textit{poly\_tags}@?, \textit{raw\_mono\_guards}@?, \\
     1.8 -\textit{raw\_mono\_tags}@? (quasi-sound):} \\
     1.9 +\textit{poly\_guards}@?, \textit{raw\_mono\_guards}@? (quasi-sound):} \\
    1.10  Alternative versions of the `\hbox{??}' encodings. As argument to the
    1.11  \textit{metis} proof method, the `\hbox{@?}' suffix is replaced by
    1.12  \hbox{``\textit{\_at\_query}''}.
    1.13 @@ -1094,8 +1093,7 @@
    1.14  
    1.15  \item[\labelitemi]
    1.16  \textbf{%
    1.17 -\textit{poly\_guards}@!, \textit{poly\_tags}@!, \textit{raw\_mono\_guards}@!, \\
    1.18 -\textit{raw\_mono\_tags}@! (mildly unsound):} \\
    1.19 +\textit{poly\_guards}@!, \textit{raw\_mono\_guards}@! (mildly unsound):} \\
    1.20  Alternative versions of the `\hbox{!!}' encodings. As argument to the
    1.21  \textit{metis} proof method, the `\hbox{@!}' suffix is replaced by
    1.22  \hbox{``\textit{\_at\_bang}''}.