1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Sun Mar 15 15:59:43 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Sun Mar 15 15:59:43 2009 +0100
     1.3 @@ -800,6 +800,7 @@
     1.4      @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
     1.5      @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
     1.6      @{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     1.7 +    @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\
     1.8    \end{matharray}
     1.9  
    1.10    \begin{mldecls}
    1.11 @@ -812,6 +813,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 @@ -856,6 +859,34 @@
    1.21    invoke local theory specification packages without going through
    1.22    concrete outer syntax, for example.
    1.23  
    1.24 +  \item @{command "attribute_setup"}~@{text "name = text description"}
    1.25 +  defines an attribute in the current theory.  The given @{text
    1.26 +  "text"} has to be an ML expression of type
    1.27 +  @{ML_type "attribute context_parser"}, cf.\ basic parsers defined in
    1.28 +  structure @{ML_struct Args} and @{ML_struct Attrib}.
    1.29 +
    1.30 +  In principle, attributes can operate both on a given theorem and the
    1.31 +  implicit context, although in practice only one is modified and the
    1.32 +  other serves as parameter.  Here are examples for these two cases:
    1.33 +
    1.34 +  \end{description}
    1.35 +*}
    1.36 +
    1.37 +    attribute_setup my_rule = {*
    1.38 +      Attrib.thms >> (fn ths =>
    1.39 +        Thm.rule_attribute (fn context: Context.generic => fn th: thm =>
    1.40 +          let val th' = th OF ths
    1.41 +          in th' end)) *}  "my rule"
    1.42 +
    1.43 +    attribute_setup my_declatation = {*
    1.44 +      Attrib.thms >> (fn ths =>
    1.45 +        Thm.declaration_attribute (fn th: thm => fn context: Context.generic =>
    1.46 +          let val context' = context
    1.47 +          in context' end)) *}  "my declaration"
    1.48 +
    1.49 +text {*
    1.50 +  \begin{description}
    1.51 +
    1.52    \item @{ML bind_thms}~@{text "(name, thms)"} stores a list of
    1.53    theorems produced in ML both in the theory context and the ML
    1.54    toplevel, associating it with the provided name.  Theorems are put