# HG changeset patch
# User wenzelm
# Date 1137881246 -3600
# Node ID b6925d782fae51f626fe655aeaacf9cd98b33e2e
# Parent  78d6ae887f6e811e308f8849c3cdf5b1b6447fa3
tuned;

diff -r 78d6ae887f6e -r b6925d782fae NEWS
--- a/NEWS	Sat Jan 21 23:02:30 2006 +0100
+++ b/NEWS	Sat Jan 21 23:07:26 2006 +0100
@@ -320,14 +320,9 @@
 * 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
+minimizing code duplication.  Thm.rule_attribute and
+Thm.declaration_attribute build canonical attributes; see also
+structure Context for further operations on Context.generic.
 
 INCOMPATIBILITY, need to adapt attribute type declarations and
 definitions.  Hint: make proper use of GenericDataFun and generic