# HG changeset patch
# User blanchet
# Date 1307515663 -7200
# Node ID 7b875e14b90d4ed7992e5df79a38869b850d9717
# Parent  30c141dc22d66466fec9418f566c807a1465046f
removed removed option from documentation

diff -r 30c141dc22d6 -r 7b875e14b90d doc-src/Sledgehammer/sledgehammer.tex
--- 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}