summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Fri, 01 Aug 2014 14:43:57 +0200 | |

changeset 57733 | bcb84750eca5 |

parent 57732 | e1b2442dc629 |

child 57734 | 18bb3e1ff6f6 |

removed proof methods as provers from docs

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