1.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex Sun Mar 15 15:59:43 2009 +0100
1.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Sun Mar 15 15:59:44 2009 +0100
1.3 @@ -808,6 +808,7 @@
1.4 \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
1.5 \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1.6 \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}} \\
1.7 + \indexdef{}{command}{attribute\_setup}\hypertarget{command.attribute-setup}{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
1.8 \end{matharray}
1.9
1.10 \begin{mldecls}
1.11 @@ -820,6 +821,8 @@
1.12 ;
1.13 ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
1.14 ;
1.15 + 'attribute\_setup' name '=' text text
1.16 + ;
1.17 \end{rail}
1.18
1.19 \begin{description}
1.20 @@ -862,6 +865,47 @@
1.21 invoke local theory specification packages without going through
1.22 concrete outer syntax, for example.
1.23
1.24 + \item \hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text\ description{\isachardoublequote}}
1.25 + defines an attribute in the current theory. The given \isa{{\isachardoublequote}text{\isachardoublequote}} has to be an ML expression of type
1.26 + \verb|attribute context_parser|, cf.\ basic parsers defined in
1.27 + structure \verb|Args| and \verb|Attrib|.
1.28 +
1.29 + In principle, attributes can operate both on a given theorem and the
1.30 + implicit context, although in practice only one is modified and the
1.31 + other serves as parameter. Here are examples for these two cases:
1.32 +
1.33 + \end{description}%
1.34 +\end{isamarkuptext}%
1.35 +\isamarkuptrue%
1.36 +%
1.37 +\isadelimML
1.38 +\ \ \ \ %
1.39 +\endisadelimML
1.40 +%
1.41 +\isatagML
1.42 +\isacommand{attribute{\isacharunderscore}setup}\isamarkupfalse%
1.43 +\ my{\isacharunderscore}rule\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
1.44 +\ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ ths\ {\isacharequal}{\isachargreater}\isanewline
1.45 +\ \ \ \ \ \ \ \ Thm{\isachardot}rule{\isacharunderscore}attribute\ {\isacharparenleft}fn\ context{\isacharcolon}\ Context{\isachardot}generic\ {\isacharequal}{\isachargreater}\ fn\ th{\isacharcolon}\ thm\ {\isacharequal}{\isachargreater}\isanewline
1.46 +\ \ \ \ \ \ \ \ \ \ let\ val\ th{\isacharprime}\ {\isacharequal}\ th\ OF\ ths\isanewline
1.47 +\ \ \ \ \ \ \ \ \ \ in\ th{\isacharprime}\ end{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ rule{\isachardoublequoteclose}\isanewline
1.48 +\isanewline
1.49 +\ \ \ \ \isacommand{attribute{\isacharunderscore}setup}\isamarkupfalse%
1.50 +\ my{\isacharunderscore}declatation\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
1.51 +\ \ \ \ \ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ ths\ {\isacharequal}{\isachargreater}\isanewline
1.52 +\ \ \ \ \ \ \ \ Thm{\isachardot}declaration{\isacharunderscore}attribute\ {\isacharparenleft}fn\ th{\isacharcolon}\ thm\ {\isacharequal}{\isachargreater}\ fn\ context{\isacharcolon}\ Context{\isachardot}generic\ {\isacharequal}{\isachargreater}\isanewline
1.53 +\ \ \ \ \ \ \ \ \ \ let\ val\ context{\isacharprime}\ {\isacharequal}\ context\isanewline
1.54 +\ \ \ \ \ \ \ \ \ \ in\ context{\isacharprime}\ end{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}\ \ {\isachardoublequoteopen}my\ declaration{\isachardoublequoteclose}%
1.55 +\endisatagML
1.56 +{\isafoldML}%
1.57 +%
1.58 +\isadelimML
1.59 +%
1.60 +\endisadelimML
1.61 +%
1.62 +\begin{isamarkuptext}%
1.63 +\begin{description}
1.64 +
1.65 \item \verb|bind_thms|~\isa{{\isachardoublequote}{\isacharparenleft}name{\isacharcomma}\ thms{\isacharparenright}{\isachardoublequote}} stores a list of
1.66 theorems produced in ML both in the theory context and the ML
1.67 toplevel, associating it with the provided name. Theorems are put
2.1 --- a/etc/isar-keywords-ZF.el Sun Mar 15 15:59:43 2009 +0100
2.2 +++ b/etc/isar-keywords-ZF.el Sun Mar 15 15:59:44 2009 +0100
2.3 @@ -31,6 +31,7 @@
2.4 "apply_end"
2.5 "arities"
2.6 "assume"
2.7 + "attribute_setup"
2.8 "axclass"
2.9 "axiomatization"
2.10 "axioms"
2.11 @@ -349,6 +350,7 @@
2.12 '("ML"
2.13 "abbreviation"
2.14 "arities"
2.15 + "attribute_setup"
2.16 "axclass"
2.17 "axiomatization"
2.18 "axioms"
3.1 --- a/etc/isar-keywords.el Sun Mar 15 15:59:43 2009 +0100
3.2 +++ b/etc/isar-keywords.el Sun Mar 15 15:59:44 2009 +0100
3.3 @@ -35,6 +35,7 @@
3.4 "atp_info"
3.5 "atp_kill"
3.6 "atp_messages"
3.7 + "attribute_setup"
3.8 "automaton"
3.9 "ax_specification"
3.10 "axclass"
3.11 @@ -421,6 +422,7 @@
3.12 "abbreviation"
3.13 "arities"
3.14 "atom_decl"
3.15 + "attribute_setup"
3.16 "automaton"
3.17 "axclass"
3.18 "axiomatization"
4.1 --- a/lib/jedit/isabelle.xml Sun Mar 15 15:59:43 2009 +0100
4.2 +++ b/lib/jedit/isabelle.xml Sun Mar 15 15:59:44 2009 +0100
4.3 @@ -61,6 +61,7 @@
4.4 <LABEL>atp_kill</LABEL>
4.5 <LABEL>atp_messages</LABEL>
4.6 <KEYWORD4>attach</KEYWORD4>
4.7 + <OPERATOR>attribute_setup</OPERATOR>
4.8 <OPERATOR>automaton</OPERATOR>
4.9 <KEYWORD4>avoids</KEYWORD4>
4.10 <OPERATOR>ax_specification</OPERATOR>