# HG changeset patch
# User wenzelm
# Date 1321734196 -3600
# Node ID 7247ade03aa9fba75cef63ec1e52ffd0d94370c0
# Parent  8baa0b7f3f66320cd4ba17e0ddeceb214dec61c3
NEWS;

diff -r 8baa0b7f3f66 -r 7247ade03aa9 NEWS
--- a/NEWS	Sat Nov 19 21:18:38 2011 +0100
+++ b/NEWS	Sat Nov 19 21:23:16 2011 +0100
@@ -4,6 +4,15 @@
 New in this Isabelle version
 ----------------------------
 
+*** General ***
+
+* Rule attributes in local theory declarations (e.g. locale or class)
+are now statically evaluated: the resulting theorem is stored instead
+of the original expression.  INCOMPATIBILITY in rare situations, where
+the historic accident of dynamic re-evaluation in interpretations
+etc. was exploited.
+
+
 *** Pure ***
 
 * Obsolete command 'types' has been discontinued.  Use 'type_synonym'
@@ -26,7 +35,6 @@
     -- "now uniform 'a::bar instead of default sort for first occurence (!)"
 
 
-
 *** HOL ***
 
 * Session HOL-Word: Discontinued many redundant theorems specific to type