# HG changeset patch
# User wenzelm
# Date 876730492 -7200
# Node ID 6061fa4637848b004318c2c1d5ab58dfdc95b758
# Parent  7fde09d61bc038fed1fe60b3e29171afeec81822
hierachically structured name spaces;

diff -r 7fde09d61bc0 -r 6061fa463784 NEWS
--- a/NEWS	Sun Oct 12 22:06:00 1997 +0200
+++ b/NEWS	Mon Oct 13 10:14:52 1997 +0200
@@ -50,6 +50,12 @@
 
 *** Syntax ***
 
+* Pure: hierachically structured name spaces (for consts, types, thms,
+...), use 'begin' or 'path' section in theory files; new lexical class
+'longid' (e.g. Foo.bar.x) renders many old input syntactically
+incorrect (e.g. "%x.x"); isatool fixdots inserts space after dots
+("%x. x");
+
 * Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories;