diff -r e87fa74113aa -r 0a3556e5d6ed NEWS
--- a/NEWS	Wed Nov 05 15:49:38 1997 +0100
+++ b/NEWS	Wed Nov 05 16:37:22 1997 +0100
@@ -7,14 +7,17 @@
 
 *** General Changes ***
 
-* hierachically structured name spaces (for consts, types, axms,
+* hierachically structured name spaces (for consts, types, axms, thms
 etc.); new lexical class 'longid' (e.g. Foo.bar.x) may render much of
 old input syntactically incorrect (e.g. "%x.x"); COMPATIBILITY:
 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 setting 'global_names' at
-compile time to disable qualified names for theories; may also fine
-tune theories via 'global' and 'local' section;
+long_names for fully qualified output names; NOTE: ML programs
+(special tactics, packages etc.) referring to internal names may have
+to be adapted to cope with fully qualified names; in case of severe
+backward campatibility problems try setting 'global_names' at compile
+time to have enrything declared within a flat name space; one may also
+fine tune name declarations in theories via the 'global' and 'local'
+section;
 
 * reimplemented the implicit simpset and claset using the new anytype
 data filed in signatures; references simpset:simpset ref etc. are
@@ -29,6 +32,8 @@
 * defs may now be conditional; improved rewrite_goals_tac to handle
 conditional equations;
 
+* defs now admits additional type arguments, using TYPE('a) syntax;
+
 * theory aliases via merge (e.g. M=A+B+C) no longer supported, always
 creates a new theory node; implicit merge of thms' signatures is
 restricted to 'trivial' ones; COMPATIBILITY: one may have to use
@@ -77,6 +82,8 @@
 
 *** Syntax ***
 
+* TYPE('a) syntax for type reflection terms;
+
 * no longer handles consts with name "" -- declare as 'syntax' instead;
 
 * pretty printer: changed order of mixfix annotation preference (again!);