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