equal
deleted
inserted
replaced
722 executable, or install the prebuilt E package from Isabelle's download page. See |
722 executable, or install the prebuilt E package from Isabelle's download page. See |
723 \S\ref{installation} for details. |
723 \S\ref{installation} for details. |
724 |
724 |
725 \item[$\bullet$] \textbf{\textit{leo2}:} LEO-II is an automatic |
725 \item[$\bullet$] \textbf{\textit{leo2}:} LEO-II is an automatic |
726 higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2}, |
726 higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2}, |
727 with support for the TPTP many-typed higher-order syntax (THF0). |
727 with support for the TPTP many-typed higher-order syntax (THF0). Sledgehammer |
|
728 requires version 1.2.9 or above. |
728 |
729 |
729 \item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than |
730 \item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than |
730 the external provers, Metis itself can be used for proof search. |
731 the external provers, Metis itself can be used for proof search. |
731 |
732 |
732 \item[$\bullet$] \textbf{\textit{metis\_full\_types}:} Fully typed version of |
733 \item[$\bullet$] \textbf{\textit{metis\_full\_types}:} Fully typed version of |