--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Dec 15 21:54:37 2008 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Dec 15 21:55:21 2008 +0100
@@ -822,6 +822,7 @@
'sledgehammer' (nameref *)
;
'atp\_messages' ('(' nat ')')?
+ ;
'metis' thmrefs
;
@@ -855,7 +856,8 @@
\item \hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}} displays recent messages issued
by automated theorem provers. This allows to examine results that
might have got lost due to the asynchronous nature of default
- \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} output.
+ \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} output. An optional message limit may
+ be specified (default 5).
\item \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} invokes the Metis prover
with the given facts. Metis is an automated proof tool of medium