tuned qualified names;
Mon, 20 Oct 1997 11:08:29 +0200
changeset 3943 b6e0c90f3bf4
parent 3942 1f1c1f524d19
child 3944 8988ba66c62b
tuned qualified names;
--- 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
+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