NEWS
changeset 41434 710cdb9e0d17
parent 41433 1b8ff770f02c
child 41435 12585dfb86fe
     1.1 --- a/NEWS	Thu Jan 06 21:06:17 2011 +0100
     1.2 +++ b/NEWS	Thu Jan 06 21:06:17 2011 +0100
     1.3 @@ -123,6 +123,11 @@
     1.4  * Document antiquotation @{file} checks file/directory entries within
     1.5  the local file system.
     1.6  
     1.7 +* Locale interpretation commands 'interpret' and 'sublocale' accept
     1.8 +equations to map definitions in a locale to appropriate entities in
     1.9 +the context of the interpretation.  The 'interpretation' command
    1.10 +already provided this functionality.
    1.11 +
    1.12  
    1.13  *** HOL ***
    1.14  
    1.15 @@ -502,8 +507,12 @@
    1.16  
    1.17  * Theorems for additive ring operations (locale abelian_monoid and
    1.18  descendants) are generated by interpretation from their multiplicative
    1.19 -counterparts.  This causes slight differences in the simp and clasets.
    1.20 -INCOMPATIBILITY.
    1.21 +counterparts.  Names (in particular theorem names) have the mandatory
    1.22 +qualifier 'add'.  Previous theorem names are redeclared for
    1.23 +compatibility.
    1.24 +
    1.25 +* Structure 'int_ring' is now an abbreviation (previously a
    1.26 +definition).  This fits more natural with advanced interpretations.
    1.27  
    1.28  
    1.29  *** HOLCF ***