NEWS
changeset 42358 b47d41d9f4b5
parent 42290 b1f544c84040
child 42360 da8817d01e7c
--- a/NEWS	Sat Apr 16 12:46:18 2011 +0200
+++ b/NEWS	Sat Apr 16 13:48:45 2011 +0200
@@ -37,6 +37,13 @@
 Note that automated detection from the file-system or search path has
 been discontinued.  INCOMPATIBILITY.
 
+* Name space: proper configuration options "long_names",
+"short_names", "unique_names" instead of former unsynchronized
+references.  Minor INCOMPATIBILITY, need to declare options in context
+like this:
+
+  declare [[unique_names = false]]
+
 
 *** HOL ***