# HG changeset patch
# User wenzelm
# Date 1287089721 -3600
# Node ID b7b1a9e8f7c2c2f64756ce38ccf2ab0aae89319c
# Parent  fc88b943e1b20dc8db8e598483d05e17aeea54da
more on "Attributes";
tuned;

diff -r fc88b943e1b2 -r b7b1a9e8f7c2 doc-src/IsarImplementation/Thy/Isar.thy
--- a/doc-src/IsarImplementation/Thy/Isar.thy	Thu Oct 14 21:05:21 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Isar.thy	Thu Oct 14 21:55:21 2010 +0100
@@ -29,11 +29,11 @@
   or @{command "by"}.
 
   \item \emph{Attributes} define a tertiary language of small
-  annotations to facts being defined or referenced.  Attributes can
-  modify both the fact and the context.
+  annotations to theorems being defined or referenced.  Attributes can
+  modify both the context and the theorem.
 
-  Typical examples are @{attribute symmetric} (which affects the
-  fact), and @{attribute intro} (which affects the context).
+  Typical examples are @{attribute intro} (which affects the context),
+  and @{attribute symmetric} (which affects the theorem).
 
   \end{enumerate}
 *}
@@ -41,7 +41,10 @@
 
 section {* Proof commands *}
 
-text {* In principle, Isar proof commands could be defined in
+text {* A \emph{proof command} is state transition of the Isar/VM
+  proof interpreter.
+
+  In principle, Isar proof commands could be defined in
   user-space as well.  The system is built like that in the first
   place: part of the commands are primitive, the other part is defined
   as derived elements.  Adding to the genuine structured proof
@@ -481,6 +484,54 @@
 
 section {* Attributes *}
 
-text FIXME
+text {* An \emph{attribute} is a function @{text "context \<times> thm \<rightarrow>
+  context \<times> thm"}, which means both a (generic) context and a theorem
+  can be modified simultaneously.  In practice this fully general form
+  is very rare, instead attributes are presented either as
+  \emph{declaration attribute:} @{text "thm \<rightarrow> context \<rightarrow> context"} or
+  \emph{rule attribute:} @{text "context \<rightarrow> thm \<rightarrow> thm"}.
+
+  Attributes can have additional arguments via concrete syntax.  There
+  is a collection of context-sensitive parsers for various logical
+  entities (types, terms, theorems).  These already take care of
+  applying morphisms to the arguments when attribute expressions are
+  moved into a different context (see also \secref{sec:morphisms}).
+
+  When implementing declaration attributes, it is important to operate
+  exactly on the variant of the generic context that is provided by
+  the system, which is either global theory context or local proof
+  context.  In particular, the background theory of a local context
+  must not be modified in this situation! *}
+
+text %mlref {*
+  \begin{mldecls}
+  @{index_ML_type attribute: "Context.generic * thm -> Context.generic * thm"} \\
+  @{index_ML Thm.rule_attribute: "(Context.generic -> thm -> thm) -> attribute"} \\
+  @{index_ML Thm.declaration_attribute: "
+  (thm -> Context.generic -> Context.generic) -> attribute"} \\
+  @{index_ML Attrib.setup: "binding -> attribute context_parser ->
+  string -> theory -> theory"} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item @{ML_type attribute} represents attributes as concrete type alias.
+
+  \item @{ML Thm.rule_attribute}~@{text "(fn context => rule)"} wraps
+  a context-dependent rule (mapping on @{ML_type thm}) as attribute.
+
+  \item @{ML Thm.declaration_attribute}~@{text "(fn thm => decl)"}
+  wraps a theorem-dependent declaration (mapping on @{ML_type
+  Context.generic}) as attribute.
+
+  \item @{ML Attrib.setup}~@{text "name parser description"} provides
+  the functionality of the Isar command @{command attribute_setup} as
+  ML function.
+
+  \end{description}
+*}
+
+text %mlex {* See also @{command attribute_setup} in
+  \cite{isabelle-isar-ref} which includes some abstract examples. *}
 
 end
diff -r fc88b943e1b2 -r b7b1a9e8f7c2 doc-src/IsarImplementation/Thy/Local_Theory.thy
--- a/doc-src/IsarImplementation/Thy/Local_Theory.thy	Thu Oct 14 21:05:21 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy	Thu Oct 14 21:55:21 2010 +0100
@@ -155,7 +155,7 @@
 *}
 
 
-section {* Morphisms and declarations *}
+section {* Morphisms and declarations \label{sec:morphisms} *}
 
 text FIXME