--- 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