# HG changeset patch
# User blanchet
# Date 1337773046 -7200
# Node ID 46c73ad5f7c034fa5f5819178a9f681dcb9a501f
# Parent  1378835671146af1477b46d2b0f2e9832ef917c6
doc updates

diff -r 137883567114 -r 46c73ad5f7c0 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Wed May 23 13:28:20 2012 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed May 23 13:37:26 2012 +0200
@@ -766,8 +766,9 @@
 \end{enum}
 
 Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options
-have a negated counterpart (e.g., \textit{blocking} vs.\
-\textit{non\_blocking}). When setting them, ``= \textit{true\/}'' may be omitted.
+have a negative counterpart (e.g., \textit{blocking} vs.\
+\textit{non\_blocking}). When setting Boolean options or their negative
+counterparts, ``= \textit{true\/}'' may be omitted.
 
 \subsection{Mode of Operation}
 \label{mode-of-operation}
@@ -1183,23 +1184,27 @@
 \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
-250.
+empirically found to be appropriate for the prover. Typical values range between
+50 and 1000.
 
-\opdefault{max\_new\_mono\_instances}{int}{\upshape 200}
+\opdefault{max\_new\_mono\_instances}{int}{smart}
 Specifies the maximum number of monomorphic instances to generate beyond
 \textit{max\_relevant}. The higher this limit is, the more monomorphic instances
 are potentially generated. Whether monomorphization takes place depends on the
-type encoding used.
+type encoding used. If the option is set to \textit{smart}, it is set to a value
+that was empirically found to be appropriate for the prover. For most provers,
+this value is 200.
 
 \nopagebreak
 {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
 
-\opdefault{max\_mono\_iters}{int}{\upshape 3}
+\opdefault{max\_mono\_iters}{int}{smart}
 Specifies the maximum number of iterations for the monomorphization fixpoint
 construction. The higher this limit is, the more monomorphic instances are
 potentially generated. Whether monomorphization takes place depends on the
-type encoding used.
+type encoding used. If the option is set to \textit{smart}, it is set to a value
+that was empirically found to be appropriate for the prover. For most provers,
+this value is 3.
 
 \nopagebreak
 {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}