--- 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