# HG changeset patch
# User wenzelm
# Date 1229373681 -3600
# Node ID fb31b7a6c8582efdc3570437bc23ef0f12528710
# Parent  f2b45eea6dac8809bd52f4a4aff596cac5e6a07a
updated generated files;

diff -r f2b45eea6dac -r fb31b7a6c858 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Dec 15 21:41:00 2008 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Dec 15 21:41:21 2008 +0100
@@ -814,12 +814,14 @@
     \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}} \\
     \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}} \\
     \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}} \\
+    \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}} \\
     \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isa{method} \\
   \end{matharray}
 
   \begin{rail}
   'sledgehammer' (nameref *)
   ;
+  'atp\_messages' ('(' nat ')')?
 
   'metis' thmrefs
   ;
@@ -850,6 +852,11 @@
   \item \hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}} terminates all presently running
   provers.
 
+  \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.
+
   \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
   strength, but is fully integrated into Isabelle/HOL, with explicit
diff -r f2b45eea6dac -r fb31b7a6c858 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Mon Dec 15 21:41:00 2008 +0100
+++ b/etc/isar-keywords-ZF.el	Mon Dec 15 21:41:21 2008 +0100
@@ -200,7 +200,6 @@
     "use"
     "use_thy"
     "using"
-    "value"
     "welcome"
     "with"
     "{"
@@ -323,7 +322,6 @@
     "typ"
     "unused_thms"
     "use_thy"
-    "value"
     "welcome"))
 
 (defconst isar-keywords-theory-begin
diff -r f2b45eea6dac -r fb31b7a6c858 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Mon Dec 15 21:41:00 2008 +0100
+++ b/etc/isar-keywords.el	Mon Dec 15 21:41:21 2008 +0100
@@ -32,6 +32,7 @@
     "atom_decl"
     "atp_info"
     "atp_kill"
+    "atp_messages"
     "automaton"
     "ax_specification"
     "axclass"
@@ -331,6 +332,7 @@
     "ML_val"
     "atp_info"
     "atp_kill"
+    "atp_messages"
     "cd"
     "class_deps"
     "code_deps"
diff -r f2b45eea6dac -r fb31b7a6c858 lib/jedit/isabelle.xml
--- a/lib/jedit/isabelle.xml	Mon Dec 15 21:41:00 2008 +0100
+++ b/lib/jedit/isabelle.xml	Mon Dec 15 21:41:21 2008 +0100
@@ -56,6 +56,7 @@
       <OPERATOR>atom_decl</OPERATOR>
       <LABEL>atp_info</LABEL>
       <LABEL>atp_kill</LABEL>
+      <LABEL>atp_messages</LABEL>
       <KEYWORD4>attach</KEYWORD4>
       <OPERATOR>automaton</OPERATOR>
       <KEYWORD4>avoids</KEYWORD4>
@@ -154,7 +155,6 @@
       <KEYWORD4>if</KEYWORD4>
       <KEYWORD4>imports</KEYWORD4>
       <KEYWORD4>in</KEYWORD4>
-      <KEYWORD4>includes</KEYWORD4>
       <KEYWORD4>induction</KEYWORD4>
       <OPERATOR>inductive</OPERATOR>
       <KEYWORD1>inductive_cases</KEYWORD1>
@@ -286,6 +286,7 @@
       <OPERATOR>statespace</OPERATOR>
       <KEYWORD4>structure</KEYWORD4>
       <OPERATOR>subclass</OPERATOR>
+      <OPERATOR>sublocale</OPERATOR>
       <OPERATOR>subsect</OPERATOR>
       <OPERATOR>subsection</OPERATOR>
       <OPERATOR>subsubsect</OPERATOR>