# HG changeset patch
# User blanchet
# Date 1327005432 -3600
# Node ID e9a2d81fa7258941504e0d82d83bb42c1bf258c2
# Parent  0a4907baf9dbded5bd9156c6150a4d63d4f96b8f
updated docs

diff -r 0a4907baf9db -r e9a2d81fa725 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Thu Jan 19 21:37:12 2012 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu Jan 19 21:37:12 2012 +0100
@@ -123,9 +123,9 @@
 Limit'' option.
 
 \newbox\boxA
-\setbox\boxA=\hbox{\texttt{nospam}}
+\setbox\boxA=\hbox{\texttt{NOSPAM}}
 
-\newcommand\authoremail{\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
+\newcommand\authoremail{\texttt{blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak
 in.\allowbreak tum.\allowbreak de}}
 
 To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is
@@ -492,10 +492,11 @@
 set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger
 value or to try several provers and keep the nicest-looking proof.
 
-\point{What are the \textit{full\_types} and \textit{no\_types} arguments to
-Metis?}
+\point{What are the \textit{full\_types}, \textit{no\_types}, and
+\textit{mono\_tags} arguments to Metis?}
 
-The \textit{metis}~(\textit{full\_types}) proof method is the fully-typed
+The \textit{metis}~(\textit{full\_types}) proof method
+and its cousin \textit{metis}~(\textit{mono\_tags}) are fully-typed
 version of Metis. It is somewhat slower than \textit{metis}, but the proof
 search is fully typed, and it also includes more powerful rules such as the
 axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in
@@ -504,16 +505,18 @@
 generated by Sledgehammer instead of \textit{metis} if the proof obviously
 requires type information or if \textit{metis} failed when Sledgehammer
 preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with
-various options for up to 4 seconds to ensure that the generated one-line proofs
-actually work and to display timing information. This can be configured using
-the \textit{preplay\_timeout} option (\S\ref{timeouts}).)
-
+various options for up to 3 seconds each time to ensure that the generated
+one-line proofs actually work and to display timing information. This can be
+configured using the \textit{preplay\_timeout} option (\S\ref{timeouts}).)
+%
 At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types})
 uses no type information at all during the proof search, which is more efficient
 but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally
 generated by Sledgehammer.
+%
+See the \textit{type\_enc} option (\S\ref{problem-encoding}) for details.
 
-Incidentally, if you see the warning
+Incidentally, if you ever see warnings such as
 
 \prew
 \slshape
@@ -523,6 +526,16 @@
 for a successful \textit{metis} proof, you can advantageously pass the
 \textit{full\_types} option to \textit{metis} directly.
 
+\point{And what are the \textit{lam\_lifting} and \textit{hide\_lams} arguments
+to Metis?}
+
+Orthogonally to the encoding of types, it is important to choose an appropriate
+translation of $\lambda$-abstractions. Metis supports three translation schemes,
+in decreasing order of power: Curry combinators (the default),
+$\lambda$-lifting, and a ``hiding'' scheme that disables all reasoning under
+$\lambda$-abstractions. The more powerful schemes also give the automatic
+provers more rope to hang themselves. See the \textit{lam\_trans} option (\S\ref{problem-encoding}) for details.
+
 \point{Are generated proofs minimal?}
 
 Automatic provers frequently use many more facts than are necessary.
@@ -683,7 +696,7 @@
 All the untyped type encodings listed in \S\ref{problem-encoding} are supported.
 For convenience, the following aliases are provided:
 \begin{enum}
-\item[\labelitemi] \textbf{\textit{full\_types}:} An appropriate type-sound encoding.
+\item[\labelitemi] \textbf{\textit{full\_types}:} Synonym for An appropriate type-sound encoding.
 \item[\labelitemi] \textbf{\textit{partial\_types}:} Synonym for \textit{poly\_args}.
 \item[\labelitemi] \textbf{\textit{no\_types}:} Synonym for \textit{erased}.
 \end{enum}
@@ -1215,7 +1228,7 @@
 For historical reasons, the default value of this option can be overridden using
 the option ``Sledgehammer: Time Limit'' in Proof General's ``Isabelle'' menu.
 
-\opdefault{preplay\_timeout}{float\_or\_none}{\upshape 4}
+\opdefault{preplay\_timeout}{float\_or\_none}{\upshape 3}
 Specifies the maximum number of seconds that \textit{metis} or \textit{smt}
 should spend trying to ``preplay'' the found proof. If this option is set to 0,
 no preplaying takes place, and no timing information is displayed next to the