src/Doc/Sledgehammer/document/root.tex

 together with a heuristic selection of hundreds of facts (theorems) from the
 current theory context, filtered by relevance.
 
 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.
 
 For Isabelle/jEdit users, Sledgehammer provides an automatic mode that can be
 enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options >

 which provers are installed and how many processor cores are available, some of
 the provers might be missing or present with a \textit{remote\_} prefix.
 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.
 
 In addition, you can ask Sledgehammer for an Isar text proof by enabling the
 \textit{isar\_proofs} option (\S\ref{output-format}):

 \prew
 \textbf{sledgehammer} [\textit{isar\_proofs}]
 \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}
 \label{hints}
 

 default, the value is prover-dependent but varies between about 50 and 1000. If
 the provers time out, you can try lowering this value to, say, 25 or 50 and see
 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}).
 
 \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
 provers' time limit. It is set to 30 seconds, but since Sledgehammer runs

 eventually find it, but that's little consolation. There are several possible
 solutions:
 
 \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
 proofs, trust the SMT solver, or use certificates. See the documentation in the
 \emph{SMT} theory (\texttt{\$ISABELLE\_HOME/src/HOL/SMT.thy}) for details.

 The \textit{metis}~(\textit{full\_types}) proof method
 and its cousin \textit{metis}~(\textit{mono\_tags}) are fully-typed
 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
 various sets of option for up to 2~seconds each time to ensure that the generated
 one-line proofs actually work and to display timing information. This can be

 MaSh is enabled; otherwise, MePo.
 \end{enum}
 
 \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
 maximum number of facts from the background library that should be learned
 ($\infty$ by default).

 
 \opdefault{max\_new\_mono\_instances}{int}{smart}
 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}).}
 
 \opdefault{max\_mono\_iters}{int}{smart}
 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}).}
 \end{enum}
 

 \nopagebreak
 {\small See also \textit{spy} (\S\ref{mode-of-operation}) and
 \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}
 is explicitly enabled. A value of $n$ indicates that each Isar proof step should
 correspond to a group of up to $n$ consecutive proof steps in the ATP proof.

 \optrue{try0\_isar}{dont\_try0\_isar}
 Specifies whether standard proof methods such as \textit{auto} and
 \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}
 \label{authentication}
 

 \opdefault{timeout}{float}{\upshape 30}
 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.
 
 \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}).}
 
 \optrueonly{dont\_preplay}