equal
deleted
inserted
replaced
820 |
820 |
821 \begin{rail} |
821 \begin{rail} |
822 'sledgehammer' (nameref *) |
822 'sledgehammer' (nameref *) |
823 ; |
823 ; |
824 'atp\_messages' ('(' nat ')')? |
824 'atp\_messages' ('(' nat ')')? |
|
825 ; |
825 |
826 |
826 'metis' thmrefs |
827 'metis' thmrefs |
827 ; |
828 ; |
828 \end{rail} |
829 \end{rail} |
829 |
830 |
853 provers. |
854 provers. |
854 |
855 |
855 \item \hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}} displays recent messages issued |
856 \item \hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}} displays recent messages issued |
856 by automated theorem provers. This allows to examine results that |
857 by automated theorem provers. This allows to examine results that |
857 might have got lost due to the asynchronous nature of default |
858 might have got lost due to the asynchronous nature of default |
858 \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} output. |
859 \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} output. An optional message limit may |
|
860 be specified (default 5). |
859 |
861 |
860 \item \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} invokes the Metis prover |
862 \item \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} invokes the Metis prover |
861 with the given facts. Metis is an automated proof tool of medium |
863 with the given facts. Metis is an automated proof tool of medium |
862 strength, but is fully integrated into Isabelle/HOL, with explicit |
864 strength, but is fully integrated into Isabelle/HOL, with explicit |
863 inferences going through the kernel. Thus its results are |
865 inferences going through the kernel. Thus its results are |