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