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