# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID b81127eb79f3af12c9cfb73802529accb804f898
# Parent  369dfc8190568dd750641764935dbefe38e06023
reflect option renaming in doc + do not document the type systems poly_preds? and poly_tags?, since they are virtually identical to the non-? versions

diff -r 369dfc819056 -r b81127eb79f3 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Thu May 12 15:29:19 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu May 12 15:29:19 2011 +0200
@@ -616,23 +616,27 @@
 \item[$\bullet$]
 \textbf{%
 \textit{simple\_types}?,
-\{\textit{poly},\textit{mono},\textit{mangled}\}\textit{\_}\{\textit{preds},\textit{tags}\}?:} \\
-The type systems \textit{poly\_preds}, \textit{poly\_tags},
-\textit{mono\_preds}, \textit{mono\_tags}, \textit{simple\_types},
+\{\textit{mono},\textit{mangled}\}\textit{\_}\{\textit{preds},\textit{tags}\}?:} \\
+The type systems \textit{mono\_preds}, \textit{mono\_tags}, \textit{simple\_types},
 \textit{mangled\_preds}, and \textit{mangled\_tags} are fully typed and
 virtually sound---except for pathological cases, all found proofs are
-type-correct. For each of these, Sledgehammer also provides a just-as-sound
-partially typed variant identified by a question mark (`{?}')\ that detects and
+type-correct. For each of these, Sledgehammer also provides a lighter (but
+virtually sound) variant identified by a question mark (`{?}')\ that detects and
 erases monotonic types, notably infinite types. (For \textit{simple\_types}, the
-types are not actually erased but rather replaced by a shared uniform type.)
+types are not actually erased but rather replaced by a shared uniform type of
+individuals.)
 
 \item[$\bullet$]
 \textbf{%
 \textit{simple\_types}!,
 \{\textit{poly},\textit{mono},\textit{mangled}\}\textit{\_}\{\textit{preds},\textit{tags}\}!:} \\
-If the question mark (`{?}')\ is replaced by an exclamation mark (`{!}'),\ the
-translation erases all types except those that are clearly finite (e.g.,
-\textit{bool}). This encoding is unsound.
+The type systems \textit{poly\_preds}, \textit{poly\_tags},
+\textit{mono\_preds}, \textit{mono\_tags}, \textit{simple\_types},
+\textit{mangled\_preds}, and \textit{mangled\_tags} also admit a somewhat
+unsound (but very efficient) variant identified by an exclamation mark (`{!}')
+that detects and erases erases all types except those that are clearly finite
+(e.g., \textit{bool}). (For \textit{simple\_types}, the types are not actually
+erased but rather replaced by a shared uniform type of individuals.)
 
 \item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled,
 uses a fully typed, virtually sound encoding; otherwise, uses any encoding. The
@@ -642,16 +646,17 @@
 
 For SMT solvers and ToFoF-E, the type system is always \textit{simple\_types}.
 
-\opdefault{max\_mono\_iters}{int}{\upshape 4}
+\opdefault{max\_mono\_iters}{int}{\upshape 5}
 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 system used.
 
-\opdefault{max\_mono\_instances}{int}{\upshape 500}
-Specifies the maximum number of monomorphic instances to generate as a soft
-limit. The higher this limit is, the more monomorphic instances are potentially
-generated. Whether monomorphization takes place depends on the type system used.
+\opdefault{max\_new\_mono\_instances}{int}{\upshape 250}
+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 system used.
 \end{enum}
 
 \subsection{Relevance Filter}