doc-src/Sledgehammer/sledgehammer.tex
changeset 43260 7b875e14b90d
parent 43229 443708f05bb2
child 43352 597f31069e18
equal deleted inserted replaced
43259:30c141dc22d6 43260:7b875e14b90d
   992 irrespective of the value of this option.
   992 irrespective of the value of this option.
   993 
   993 
   994 \nopagebreak
   994 \nopagebreak
   995 {\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter})
   995 {\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter})
   996 and \textit{max\_mono\_iters} (\S\ref{relevance-filter}).}
   996 and \textit{max\_mono\_iters} (\S\ref{relevance-filter}).}
   997 
       
   998 \opsmart{explicit\_apply}{implicit\_apply}
       
   999 Specifies whether function application should be encoded as an explicit
       
  1000 ``apply'' operator in ATP problems. If the option is set to \textit{false}, each
       
  1001 function will be directly applied to as many arguments as possible. Disabling
       
  1002 this option can sometimes prevent the discovery of higher-order proofs.
       
  1003 \end{enum}
   997 \end{enum}
  1004 
   998 
  1005 \subsection{Relevance Filter}
   999 \subsection{Relevance Filter}
  1006 \label{relevance-filter}
  1000 \label{relevance-filter}
  1007 
  1001