# HG changeset patch
# User wenzelm
# Date 877338509 -7200
# Node ID b6e0c90f3bf45b1dd1e1e2941321ec85c059bb2c
# Parent  1f1c1f524d196944402eec6ad53e4c0f1d00618e
tuned qualified names;

diff -r 1f1c1f524d19 -r b6e0c90f3bf4 NEWS
--- 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