# HG changeset patch
# User wenzelm
# Date 1237129184 -3600
# Node ID fae488569faf762e6029c067f112a158fc501703
# Parent  7f9a9ec1c94d8c0e748629472b24632b691db39d
updated generated files;

diff -r 7f9a9ec1c94d -r fae488569faf doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Sun Mar 15 15:59:43 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sun Mar 15 15:59:44 2009 +0100
@@ -808,6 +808,7 @@
     \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
     \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     \indexdef{}{command}{local\_setup}\hypertarget{command.local-setup}{\hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
+    \indexdef{}{command}{attribute\_setup}\hypertarget{command.attribute-setup}{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   \end{matharray}
 
   \begin{mldecls}
@@ -820,6 +821,8 @@
     ;
     ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
     ;
+    'attribute\_setup' name '=' text text
+    ;
   \end{rail}
 
   \begin{description}
@@ -862,6 +865,47 @@
   invoke local theory specification packages without going through
   concrete outer syntax, for example.
 
+  \item \hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}
+  defines an attribute in the current theory.  The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type
+  \verb|attribute context_parser|, cf.\ basic parsers defined in
+  structure \verb|Args| and \verb|Attrib|.
+
+  In principle, attributes can operate both on a given theorem and the
+  implicit context, although in practice only one is modified and the
+  other serves as parameter.  Here are examples for these two cases:
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+\ \ \ \ %
+\endisadelimML
+%
+\isatagML
+\isacommand{attribute{\isacharunderscore}setup}\isamarkupfalse%
+\ my{\isacharunderscore}rule\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
+\ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ ths\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ Thm{\isachardot}rule{\isacharunderscore}attribute\ {\isacharparenleft}fn\ context{\isacharcolon}\ Context{\isachardot}generic\ {\isacharequal}{\isachargreater}\ fn\ th{\isacharcolon}\ thm\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ \ \ let\ val\ th{\isacharprime}\ {\isacharequal}\ th\ OF\ ths\isanewline
+\ \ \ \ \ \ \ \ \ \ in\ th{\isacharprime}\ end{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ rule{\isachardoublequoteclose}\isanewline
+\isanewline
+\ \ \ \ \isacommand{attribute{\isacharunderscore}setup}\isamarkupfalse%
+\ my{\isacharunderscore}declatation\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
+\ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ ths\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ Thm{\isachardot}declaration{\isacharunderscore}attribute\ {\isacharparenleft}fn\ th{\isacharcolon}\ thm\ {\isacharequal}{\isachargreater}\ fn\ context{\isacharcolon}\ Context{\isachardot}generic\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ \ \ let\ val\ context{\isacharprime}\ {\isacharequal}\ context\isanewline
+\ \ \ \ \ \ \ \ \ \ in\ context{\isacharprime}\ end{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ declaration{\isachardoublequoteclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+\begin{description}
+
   \item \verb|bind_thms|~\isa{{\isachardoublequote}{\isacharparenleft}name{\isacharcomma}\ thms{\isacharparenright}{\isachardoublequote}} stores a list of
   theorems produced in ML both in the theory context and the ML
   toplevel, associating it with the provided name.  Theorems are put
diff -r 7f9a9ec1c94d -r fae488569faf etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Sun Mar 15 15:59:43 2009 +0100
+++ b/etc/isar-keywords-ZF.el	Sun Mar 15 15:59:44 2009 +0100
@@ -31,6 +31,7 @@
     "apply_end"
     "arities"
     "assume"
+    "attribute_setup"
     "axclass"
     "axiomatization"
     "axioms"
@@ -349,6 +350,7 @@
   '("ML"
     "abbreviation"
     "arities"
+    "attribute_setup"
     "axclass"
     "axiomatization"
     "axioms"
diff -r 7f9a9ec1c94d -r fae488569faf etc/isar-keywords.el
--- a/etc/isar-keywords.el	Sun Mar 15 15:59:43 2009 +0100
+++ b/etc/isar-keywords.el	Sun Mar 15 15:59:44 2009 +0100
@@ -35,6 +35,7 @@
     "atp_info"
     "atp_kill"
     "atp_messages"
+    "attribute_setup"
     "automaton"
     "ax_specification"
     "axclass"
@@ -421,6 +422,7 @@
     "abbreviation"
     "arities"
     "atom_decl"
+    "attribute_setup"
     "automaton"
     "axclass"
     "axiomatization"
diff -r 7f9a9ec1c94d -r fae488569faf lib/jedit/isabelle.xml
--- a/lib/jedit/isabelle.xml	Sun Mar 15 15:59:43 2009 +0100
+++ b/lib/jedit/isabelle.xml	Sun Mar 15 15:59:44 2009 +0100
@@ -61,6 +61,7 @@
       <LABEL>atp_kill</LABEL>
       <LABEL>atp_messages</LABEL>
       <KEYWORD4>attach</KEYWORD4>
+      <OPERATOR>attribute_setup</OPERATOR>
       <OPERATOR>automaton</OPERATOR>
       <KEYWORD4>avoids</KEYWORD4>
       <OPERATOR>ax_specification</OPERATOR>