--- 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
--- 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
--- 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"
--- 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>