doc-src/Sledgehammer/sledgehammer.tex
changeset 43260 7b875e14b90d
parent 43229 443708f05bb2
child 43352 597f31069e18
--- 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}