# HG changeset patch
# User blanchet
# Date 1306767638 -7200
# Node ID d1e547e25be2843028d551c8a2c3aae2f8153f72
# Parent  b6e61d22fa61d05466d153c1d11c9fe945041a15
document new explicit apply

diff -r b6e61d22fa61 -r d1e547e25be2 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Mon May 30 17:00:38 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Mon May 30 17:00:38 2011 +0200
@@ -663,7 +663,6 @@
 \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{true}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
 \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\enskip \defl\textit{false}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
 \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
-\def\opsmartx#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{smart\_bool}$\bigr]$\enskip \defl\textit{smart}\defr\hfill\\\hbox{}\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
 \def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
 \def\opnodefaultbrk#1#2{\flushitem{$\bigl[$\textit{#1} =$\bigr]$ \qtybf{#2}} \nopagebreak\\[\parskip]}
 \def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\enskip \defl\textit{#3}\defr} \nopagebreak\\[\parskip]}
@@ -866,13 +865,6 @@
 \label{problem-encoding}
 
 \begin{enum}
-\opfalse{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. Enabling
-this option can sometimes help discover higher-order proofs that otherwise would
-not be found.
-
 \opfalse{full\_types}{partial\_types}
 Specifies whether full type information is encoded in ATP problems. Enabling
 this option prevents the discovery of type-incorrect proofs, but it can slow
@@ -974,6 +966,12 @@
 \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}
@@ -988,11 +986,11 @@
 iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems
 are relevant and 1 only theorems that refer to previously seen constants.
 
-\opsmart{max\_relevant}{smart\_int}
+\opdefault{max\_relevant}{smart\_int}{smart}
 Specifies the maximum number of facts that may be returned by the relevance
 filter. If the option is set to \textit{smart}, it is set to a value that was
 empirically found to be appropriate for the prover. A typical value would be
-300.
+250.
 
 \opdefault{max\_new\_mono\_instances}{int}{\upshape 400}
 Specifies the maximum number of monomorphic instances to generate beyond