--- a/NEWS Mon Oct 20 11:06:01 1997 +0200
+++ b/NEWS Mon Oct 20 11:08:29 1997 +0200
@@ -1,3 +1,4 @@
+
Isabelle NEWS -- history of user-visible changes
================================================
@@ -7,11 +8,13 @@
*** General Changes ***
* hierachically structured name spaces (for consts, types, axms,
-etc.); use 'begin' or 'path' section in theory files; new lexical
-class 'longid' (e.g. Foo.bar.x) may render much of old input
-syntactically incorrect (e.g. "%x.x"); isatool fixdots ensures space
-after dots (e.g. "%x. x"); set long_names for fully qualified output
-names;
+etc.); new lexical class 'longid' (e.g. Foo.bar.x) may render much of
+old input syntactically incorrect (e.g. "%x.x"); isatool fixdots
+ensures space after dots (e.g. "%x. x"); set long_names for fully
+qualified output names; NOTE: in case of severe problems with backward
+campatibility try settin 'global_names' at compile time to disable
+qualified names for theories; may also fine tune theories via 'global'
+and 'local' section;
* HTML output now includes theory graph data for display with Java
applet or isatool browser; data generated automatically via isatool