--- a/NEWS Thu Apr 02 14:02:45 2009 +0200
+++ b/NEWS Thu Apr 02 14:09:41 2009 +0200
@@ -52,7 +52,6 @@
as hyperlinks are now available uniformly.
-
*** Pure ***
* Complete re-implementation of locales. INCOMPATIBILITY in several
@@ -612,6 +611,12 @@
one_not_zero ~> carrier_one_not_zero (collision with assumption)
+*** HOL-Nominal ***
+
+* Modernized versions of commands 'nominal_inductive',
+'nominal_primrec', and 'equivariance' work with local theory targets.
+
+
*** HOLCF ***
* Reimplemented the simplification procedure for proving continuity