# HG changeset patch
# User wenzelm
# Date 1137880950 -3600
# Node ID 78d6ae887f6e811e308f8849c3cdf5b1b6447fa3
# Parent  541d04c79e124df76aa4a4c88bf2adc2daefa671
* ML: simplified type attribute;

diff -r 541d04c79e12 -r 78d6ae887f6e NEWS
--- 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