doc-src/Sledgehammer/sledgehammer.tex

 Sledgehammer is run on every newly entered theorem. The time limit for Auto
 Sledgehammer and other automatic tools can be set using the ``Auto Tools Time
 Limit'' option.
 
 \newbox\boxA
-\setbox\boxA=\hbox{\texttt{nospam}}
-
-\newcommand\authoremail{\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
+\setbox\boxA=\hbox{\texttt{NOSPAM}}
+
+\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
 imported---this is rarely a problem in practice since it is part of
 \textit{Main}. Examples of Sledgehammer use can be found in Isabelle's

 research into transforming resolution proofs into natural deduction proofs (such
 as Isar proofs), which we hope to leverage. In the meantime, a workaround is to
 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?}
-
-The \textit{metis}~(\textit{full\_types}) proof method is the fully-typed
+\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
+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
 higher-order places (e.g., in set comprehensions). The method kicks in
 automatically as a fallback when \textit{metis} fails, and it is sometimes
 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.
-
-Incidentally, if you see the warning
+%
+See the \textit{type\_enc} option (\S\ref{problem-encoding}) for details.
+
+Incidentally, if you ever see warnings such as
 
 \prew
 \slshape
 Metis: Falling back on ``\textit{metis} (\textit{full\_types})''.
 \postw
 
 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.
 Sledgehammer inclues a minimization tool that takes a set of facts returned by a

 \textit{lam\_lifting}, and \textit{combinators} (the default).
 %
 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}
 
 \section{Option Reference}

 Specifies the maximum number of seconds that the automatic provers should spend
 searching for a proof. This excludes problem preparation and is a soft limit.
 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
 suggested \textit{metis} calls.