updated generated file;
authorwenzelm
Mon Dec 15 21:55:21 2008 +0100 (2008-12-15)
changeset 291156fb7be34506e
parent 29114 715178f6ae31
child 29116 d9e423b9e707
updated generated file;
doc-src/IsarRef/Thy/document/HOL_Specific.tex
     1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Dec 15 21:54:37 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Dec 15 21:55:21 2008 +0100
     1.3 @@ -822,6 +822,7 @@
     1.4    'sledgehammer' (nameref *)
     1.5    ;
     1.6    'atp\_messages' ('(' nat ')')?
     1.7 +  ;
     1.8  
     1.9    'metis' thmrefs
    1.10    ;
    1.11 @@ -855,7 +856,8 @@
    1.12    \item \hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}} displays recent messages issued
    1.13    by automated theorem provers.  This allows to examine results that
    1.14    might have got lost due to the asynchronous nature of default
    1.15 -  \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} output.
    1.16 +  \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} output.  An optional message limit may
    1.17 +  be specified (default 5).
    1.18  
    1.19    \item \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} invokes the Metis prover
    1.20    with the given facts.  Metis is an automated proof tool of medium