# HG changeset patch
# User wenzelm
# Date 1229374521 -3600
# Node ID 6fb7be34506eb23a9339b538a3fd86ef5d6ddda0
# Parent  715178f6ae3127f12790c229797206c2d2c8b215
updated generated file;

diff -r 715178f6ae31 -r 6fb7be34506e doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- 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