doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 29112 f2b45eea6dac
parent 28761 9ec4482c9201
child 29114 715178f6ae31
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Dec 15 10:19:02 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Dec 15 21:41:00 2008 +0100
     1.3 @@ -804,12 +804,14 @@
     1.4      @{command_def (HOL) "print_atps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     1.5      @{command_def (HOL) "atp_info"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
     1.6      @{command_def (HOL) "atp_kill"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
     1.7 +    @{command_def (HOL) "atp_messages"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
     1.8      @{method_def (HOL) metis} & : & @{text method} \\
     1.9    \end{matharray}
    1.10  
    1.11    \begin{rail}
    1.12    'sledgehammer' (nameref *)
    1.13    ;
    1.14 +  'atp\_messages' ('(' nat ')')?
    1.15  
    1.16    'metis' thmrefs
    1.17    ;
    1.18 @@ -842,6 +844,12 @@
    1.19    \item @{command (HOL) atp_kill} terminates all presently running
    1.20    provers.
    1.21  
    1.22 +  \item @{command (HOL) atp_messages} displays recent messages issued
    1.23 +  by automated theorem provers.  This allows to examine results that
    1.24 +  might have got lost due to the asynchronous nature of default
    1.25 +  @{command (HOL) sledgehammer} output.  An optional message limit may
    1.26 +  be specified (default 5).
    1.27 +
    1.28    \item @{method (HOL) metis}~@{text "facts"} invokes the Metis prover
    1.29    with the given facts.  Metis is an automated proof tool of medium
    1.30    strength, but is fully integrated into Isabelle/HOL, with explicit