NEWS;
authorwenzelm
Sat Nov 19 21:23:16 2011 +0100 (2011-11-19)
changeset 455937247ade03aa9
parent 45592 8baa0b7f3f66
child 45594 d320f2f9f331
NEWS;
NEWS
     1.1 --- a/NEWS	Sat Nov 19 21:18:38 2011 +0100
     1.2 +++ b/NEWS	Sat Nov 19 21:23:16 2011 +0100
     1.3 @@ -4,6 +4,15 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** General ***
     1.8 +
     1.9 +* Rule attributes in local theory declarations (e.g. locale or class)
    1.10 +are now statically evaluated: the resulting theorem is stored instead
    1.11 +of the original expression.  INCOMPATIBILITY in rare situations, where
    1.12 +the historic accident of dynamic re-evaluation in interpretations
    1.13 +etc. was exploited.
    1.14 +
    1.15 +
    1.16  *** Pure ***
    1.17  
    1.18  * Obsolete command 'types' has been discontinued.  Use 'type_synonym'
    1.19 @@ -26,7 +35,6 @@
    1.20      -- "now uniform 'a::bar instead of default sort for first occurence (!)"
    1.21  
    1.22  
    1.23 -
    1.24  *** HOL ***
    1.25  
    1.26  * Session HOL-Word: Discontinued many redundant theorems specific to type