--- 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).
--- 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 ***