--- a/src/Doc/Sledgehammer/document/root.tex Mon Feb 03 19:32:02 2014 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Mon Feb 03 19:32:02 2014 +0100
@@ -117,7 +117,7 @@
The result of a successful proof search is some source text that usually (but
not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed
-proof relies on the general-purpose \textit{metis} proof method, which
+proof typically relies on the general-purpose \textit{metis} proof method, which
integrates the Metis ATP in Isabelle/HOL with explicit inferences going through
the kernel. Thus its results are correct by construction.
@@ -296,7 +296,7 @@
Waldmeister is run only for unit equational problems, where the goal's
conclusion is a (universally quantified) equation.
-For each successful prover, Sledgehammer gives a one-liner \textit{metis} or
+For each successful prover, Sledgehammer gives a one-line \textit{metis} or
\textit{smt} method call. Rough timings are shown in parentheses, indicating how
fast the call is. You can click the proof to insert it into the theory text.
@@ -308,7 +308,7 @@
\postw
When Isar proof construction is successful, it can yield proofs that are more
-readable and also faster than the \textit{metis} or \textit{smt} one-liners.
+readable and also faster than the \textit{metis} or \textit{smt} one-line proofs.
This feature is experimental and is only available for ATPs.
\section{Hints}
@@ -359,7 +359,7 @@
if that helps.
\item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
-that Isar proofs should be generated, in addition to one-liner \textit{metis} or
+that Isar proofs should be generated, in addition to one-line \textit{metis} or
\textit{smt} proofs. The length of the Isar proofs can be controlled by setting
\textit{compress\_isar} (\S\ref{output-format}).
@@ -463,9 +463,8 @@
\begin{enum}
\item[\labelitemi] Try the \textit{isar\_proofs} option (\S\ref{output-format}) to
-obtain a step-by-step Isar proof where each step is justified by \textit{metis}.
-Since the steps are fairly small, \textit{metis} is more likely to be able to
-replay them.
+obtain a step-by-step Isar proof. Since the steps are fairly small, \textit{metis}
+and the other Isabelle proof methods are more likely to be able to replay them.
\item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}.
It is usually stronger, but you need to either have Z3 available to replay the
@@ -525,8 +524,8 @@
versions 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
+higher-order places (e.g., in set comprehensions). The method is automatically
+tried 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
@@ -1069,9 +1068,9 @@
\opdefault{max\_facts}{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 effectively takes a value
-that was empirically found to be appropriate for the prover. Typical values
-range between 50 and 1000.
+filter. If the option is set to \textit{smart} (the default), it effectively
+takes a value that was empirically found to be appropriate for the prover.
+Typical values range between 50 and 1000.
For the MaSh-related commands \textit{learn\_isar}, \textit{learn\_prover},
\textit{relearn\_isar}, and \textit{relearn\_prover}, this option specifies the
@@ -1095,9 +1094,9 @@
Specifies the maximum number of monomorphic instances to generate beyond
\textit{max\_facts}. The higher this limit is, the more monomorphic instances
are potentially generated. Whether monomorphization takes place depends on the
-type encoding used. If the option is set to \textit{smart}, it takes a value
-that was empirically found to be appropriate for the prover. For most provers,
-this value is 100.
+type encoding used. If the option is set to \textit{smart} (the default), it
+takes a value that was empirically found to be appropriate for the prover. For
+most provers, this value is 100.
\nopagebreak
{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
@@ -1106,9 +1105,9 @@
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. If the option is set to \textit{smart}, it takes a value
-that was empirically found to be appropriate for the prover. For most provers,
-this value is 3.
+type encoding used. If the option is set to \textit{smart} (the default), it
+takes 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}).}
@@ -1298,12 +1297,11 @@
\textit{overlord} (\S\ref{mode-of-operation}).}
\opsmart{isar\_proofs}{no\_isar\_proofs}
-Specifies whether Isar proofs should be output in addition to one-liner
-\textit{metis} proofs. The construction of Isar proof is still experimental and
-may sometimes fail; however, when they succeed they are usually faster and more
-intelligible than \textit{metis} proofs. If the option is set to \textit{smart}
-(the default), Isar proofs are only generated when no working one-liner
-\textit{metis} proof is available.
+Specifies whether Isar proofs should be output in addition to one-line proofs.
+The construction of Isar proof is still experimental and may sometimes fail;
+however, when they succeed they are usually faster and more intelligible than
+one-line proofs. If the option is set to \textit{smart} (the default), Isar
+proofs are only generated when no working one-line proof is available.
\opdefault{compress\_isar}{int}{\upshape 10}
Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
@@ -1318,10 +1316,11 @@
\textit{blast} should be tried as alternatives to \textit{metis} in Isar proofs.
The collection of methods is roughly the same as for the \textbf{try0} command.
-\opsmart{smt}{no\_smt}
+\opsmart{smt\_proofs}{no\_smt\_proofs}
Specifies whether the \textit{smt} proof method should be tried as an
-alternative to \textit{metis}. If the option is set to \textit{smart}, the
-\textit{smt} method is used for one-line proofs but not in Isar proofs.
+alternative to \textit{metis}. If the option is set to \textit{smart} (the
+default), the \textit{smt} method is used for one-line proofs but not in Isar
+proofs.
\end{enum}
\subsection{Authentication}
@@ -1357,10 +1356,10 @@
searching for a proof. This excludes problem preparation and is a soft limit.
\opdefault{preplay\_timeout}{float}{\upshape 2}
-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.
+Specifies the maximum number of seconds that \textit{metis} or other proof
+methods 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 proof method calls.
\nopagebreak
{\small See also \textit{minimize} (\S\ref{mode-of-operation}).}