1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Dec 15 21:41:00 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Dec 15 21:41:21 2008 +0100
     1.3 @@ -814,12 +814,14 @@
     1.4      \indexdef{HOL}{command}{print\_atps}\hypertarget{command.HOL.print-atps}{\hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
     1.5      \indexdef{HOL}{command}{atp\_info}\hypertarget{command.HOL.atp-info}{\hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
     1.6      \indexdef{HOL}{command}{atp\_kill}\hypertarget{command.HOL.atp-kill}{\hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
     1.7 +    \indexdef{HOL}{command}{atp\_messages}\hypertarget{command.HOL.atp-messages}{\hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
     1.8      \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isa{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 @@ -850,6 +852,11 @@
    1.19    \item \hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}} terminates all presently running
    1.20    provers.
    1.21  
    1.22 +  \item \hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}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 +  \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} output.
    1.26 +
    1.27    \item \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} invokes the Metis prover
    1.28    with the given facts.  Metis is an automated proof tool of medium
    1.29    strength, but is fully integrated into Isabelle/HOL, with explicit

     2.1 --- a/etc/isar-keywords-ZF.el	Mon Dec 15 21:41:00 2008 +0100
     2.2 +++ b/etc/isar-keywords-ZF.el	Mon Dec 15 21:41:21 2008 +0100
     2.3 @@ -200,7 +200,6 @@
     2.4      "use"
     2.5      "use_thy"
     2.6      "using"
     2.7 -    "value"
     2.8      "welcome"
     2.9      "with"
    2.10      "{"
    2.11 @@ -323,7 +322,6 @@
    2.12      "typ"
    2.13      "unused_thms"
    2.14      "use_thy"
    2.15 -    "value"
    2.16      "welcome"))
    2.17  
    2.18  (defconst isar-keywords-theory-begin

     3.1 --- a/etc/isar-keywords.el	Mon Dec 15 21:41:00 2008 +0100
     3.2 +++ b/etc/isar-keywords.el	Mon Dec 15 21:41:21 2008 +0100
     3.3 @@ -32,6 +32,7 @@
     3.4      "atom_decl"
     3.5      "atp_info"
     3.6      "atp_kill"
     3.7 +    "atp_messages"
     3.8      "automaton"
     3.9      "ax_specification"
    3.10      "axclass"
    3.11 @@ -331,6 +332,7 @@
    3.12      "ML_val"
    3.13      "atp_info"
    3.14      "atp_kill"
    3.15 +    "atp_messages"
    3.16      "cd"
    3.17      "class_deps"
    3.18      "code_deps"

     4.1 --- a/lib/jedit/isabelle.xml	Mon Dec 15 21:41:00 2008 +0100
     4.2 +++ b/lib/jedit/isabelle.xml	Mon Dec 15 21:41:21 2008 +0100
     4.3 @@ -56,6 +56,7 @@
     4.4        <OPERATOR>atom_decl</OPERATOR>
     4.5        <LABEL>atp_info</LABEL>
     4.6        <LABEL>atp_kill</LABEL>
     4.7 +      <LABEL>atp_messages</LABEL>
     4.8        <KEYWORD4>attach</KEYWORD4>
     4.9        <OPERATOR>automaton</OPERATOR>
    4.10        <KEYWORD4>avoids</KEYWORD4>
    4.11 @@ -154,7 +155,6 @@
    4.12        <KEYWORD4>if</KEYWORD4>
    4.13        <KEYWORD4>imports</KEYWORD4>
    4.14        <KEYWORD4>in</KEYWORD4>
    4.15 -      <KEYWORD4>includes</KEYWORD4>
    4.16        <KEYWORD4>induction</KEYWORD4>
    4.17        <OPERATOR>inductive</OPERATOR>
    4.18        <KEYWORD1>inductive_cases</KEYWORD1>
    4.19 @@ -286,6 +286,7 @@
    4.20        <OPERATOR>statespace</OPERATOR>
    4.21        <KEYWORD4>structure</KEYWORD4>
    4.22        <OPERATOR>subclass</OPERATOR>
    4.23 +      <OPERATOR>sublocale</OPERATOR>
    4.24        <OPERATOR>subsect</OPERATOR>
    4.25        <OPERATOR>subsection</OPERATOR>
    4.26        <OPERATOR>subsubsect</OPERATOR>