# HG changeset patch
# User wenzelm
# Date 1193081526 -7200
# Node ID 9c9646c1080d673c5c1149aef0f3a0afa3d1705f
# Parent  85463aff6dbe693ef5255b778db305cb9693b836
tuned Nominal entry;

diff -r 85463aff6dbe -r 9c9646c1080d ANNOUNCE
--- a/ANNOUNCE	Mon Oct 22 16:54:54 2007 +0200
+++ b/ANNOUNCE	Mon Oct 22 21:32:06 2007 +0200
@@ -11,8 +11,8 @@
 
 The main highlights are:
 
-* Fully featured support for nominal datatypes (binding structures)
-due to the HOL-Nominal logic.
+* Support for nominal datatypes (binding structures) due to the
+HOL-Nominal logic.
 
 * General local theory infrastructure for specifications depending on
 parameters and assumptions (e.g. from locales, classes).
diff -r 85463aff6dbe -r 9c9646c1080d NEWS
--- a/NEWS	Mon Oct 22 16:54:54 2007 +0200
+++ b/NEWS	Mon Oct 22 21:32:06 2007 +0200
@@ -1200,14 +1200,11 @@
 
 *** HOL-Nominal ***
 
-* Not yet complete support for nominal datatypes (binding structures)
-based on HOL-Nominal logic. See HOL/Nominal and HOL/Nominal/Examples.
-If you plan to use nominal datatypes you are strongly advised to
-visit 
-
- http://isabelle.in.tum.de/nominal/
-
-and look there for up-to-date information.
+* Substantial, yet incomplete support for nominal datatypes (binding
+structures) based on HOL-Nominal logic.  See HOL/Nominal and
+HOL/Nominal/Examples.  Prespective users should consult
+http://isabelle.in.tum.de/nominal/
+
 
 *** ML ***