--- a/NEWS Sat Jan 21 23:02:29 2006 +0100
+++ b/NEWS Sat Jan 21 23:02:30 2006 +0100
@@ -317,11 +317,21 @@
provides some facilities for code that works in either kind of
context, notably GenericDataFun for uniform theory and proof data.
-* Pure: type Context.generic attribute is now the preferred
-representation for global vs. local attributes while avoiding code
-duplication; Attrib.theory/context/generic converts between different
-types of attributes. Various Pure/HOL/ZF packages work with generic
-attributes now, INCOMPATIBILITY.
+* Pure: simplified internal attribute type, which is now always
+Context.generic * thm -> Context.generic * thm. Global (theory)
+vs. local (Proof.context) attributes have been discontinued, while
+minimizing code duplication. The following basic operations build and
+apply attributes (see also structure Context for further operations on
+Context.generic):
+
+ Thm.rule_attribute: (Context.generic -> thm -> thm) -> attribute
+ Thm.declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
+ Thm.theory_attributes: attribute list -> theory * thm -> theory * thm
+ Thm.proof_attributes: attribute list -> Context.proof * thm -> Context.proof * thm
+
+INCOMPATIBILITY, need to adapt attribute type declarations and
+definitions. Hint: make proper use of GenericDataFun and generic
+Args/Attrib syntax instead of working around legacy code.
* Pure: several functions of signature "... -> theory -> theory * ..."
have been reoriented to "... -> theory -> ... * theory" in order to