# HG changeset patch # User blanchet # Date 1406897037 -7200 # Node ID bcb84750eca593808f09040b1e4fdbbe025766f8 # Parent e1b2442dc629825b1e0fabc1ce62859b6c96342c removed proof methods as provers from docs diff -r e1b2442dc629 -r bcb84750eca5 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Fri Aug 01 14:43:57 2014 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Fri Aug 01 14:43:57 2014 +0200 @@ -453,8 +453,8 @@ \begin{enum} \item[\labelitemi] Try the \textit{isar\_proofs} option (\S\ref{output-format}) to -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. +obtain a step-by-step Isar proof. Since the steps are fairly small, Isabelle's +proof methods are more likely to be able to replay them. \item[\labelitemi] Try the \textit{smt2} proof method instead of \textit{metis}. It is usually stronger, but you need to either have Z3 available to replay the @@ -962,15 +962,8 @@ SPASS, and Vampire for 5~seconds yields a similar success rate to running the most effective of these for 120~seconds \cite{boehme-nipkow-2010}. -In addition to the local and remote provers, the Isabelle proof methods -\textit{metis} and \textit{smt2} can be specified as \textbf{\textit{metis}} -and \textbf{\textit{smt}}, respectively. They are generally not recommended -for proof search but occasionally arise in Sledgehammer-generated -minimization commands (e.g., -``\textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{metis}]''). - -For the \textit{min} subcommand, the default prover is \textit{metis}. If -several provers are set, the first one is used. +For the \textit{min} subcommand, the first prover is used if several are +specified. \opnodefault{prover}{string} Alias for \textit{provers}. @@ -1321,8 +1314,8 @@ The collection of methods is roughly the same as for the \textbf{try0} command. \opsmart{smt\_proofs}{no\_smt\_proofs} -Specifies whether the \textit{smt2} proof method should be tried as an -alternative to \textit{metis}. If the option is set to \textit{smart} (the +Specifies whether the \textit{smt2} proof method should be tried in addition to +Isabelle's other proof methods. If the option is set to \textit{smart} (the default), the \textit{smt2} method is used for one-line proofs but not in Isar proofs. \end{enum}