1.1 --- a/NEWS	Thu Apr 02 14:02:45 2009 +0200
     1.2 +++ b/NEWS	Thu Apr 02 14:09:41 2009 +0200
     1.3 @@ -52,7 +52,6 @@
     1.4  as hyperlinks are now available uniformly.
     1.5  
     1.6  
     1.7 -
     1.8  *** Pure ***
     1.9  
    1.10  * Complete re-implementation of locales.  INCOMPATIBILITY in several
    1.11 @@ -612,6 +611,12 @@
    1.12  one_not_zero ~> carrier_one_not_zero  (collision with assumption)
    1.13  
    1.14  
    1.15 +*** HOL-Nominal ***
    1.16 +
    1.17 +* Modernized versions of commands 'nominal_inductive',
    1.18 +'nominal_primrec', and 'equivariance' work with local theory targets.
    1.19 +
    1.20 +
    1.21  *** HOLCF ***
    1.22  
    1.23  * Reimplemented the simplification procedure for proving continuity