1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Wed Jun 08 08:47:43 2011 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed Jun 08 08:47:43 2011 +0200
     1.3 @@ -994,12 +994,6 @@
     1.4  \nopagebreak
     1.5  {\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter})
     1.6  and \textit{max\_mono\_iters} (\S\ref{relevance-filter}).}
     1.7 -
     1.8 -\opsmart{explicit\_apply}{implicit\_apply}
     1.9 -Specifies whether function application should be encoded as an explicit
    1.10 -``apply'' operator in ATP problems. If the option is set to \textit{false}, each
    1.11 -function will be directly applied to as many arguments as possible. Disabling
    1.12 -this option can sometimes prevent the discovery of higher-order proofs.
    1.13  \end{enum}
    1.14  
    1.15  \subsection{Relevance Filter}