# HG changeset patch
# User wenzelm
# Date 1238674181 -7200
# Node ID 0e5ec6d2c1d95abea0372b5c2c8900d588423afe
# Parent  c57b57546a07b90295f1b0ca9dbfb89a23c5108e
some HOL-Nominal news;

diff -r c57b57546a07 -r 0e5ec6d2c1d9 NEWS
--- 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