# HG changeset patch
# User wenzelm
# Date 877006355 -7200
# Node ID 8b09bc500f655170e03471baafb753d857fa1e60
# Parent  e30bd27a49103006979be333794ea1ba9cc4fd2c
tuned;

diff -r e30bd27a4910 -r 8b09bc500f65 NEWS
--- a/NEWS	Thu Oct 16 14:48:10 1997 +0200
+++ b/NEWS	Thu Oct 16 14:52:35 1997 +0200
@@ -7,20 +7,30 @@
 
 *** General Changes ***
 
-* 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 much of old input syntactically
-incorrect (e.g. "%x.x"); isatool fixdots inserts space after dots
-("%x. x");
+* 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;
 
 * HTML output now includes theory graph data for display with Java
 applet or isatool browser; data generated automatically via isatool
-usedir (see -i option);
+usedir (see -i option, ISABELLE_USEDIR_OPTIONS);
 
 * defs may now be conditional; improved rewrite_goals_tac to handle
 conditional equations;
 
-* print_goals: optional output of const types (set show_consts);
+* 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, thus one may have to use
+transfer:theory->thm->thm in (rare) cases;
+
+* slightly changed interfaces for oracles: admit many per theory, named
+(e.g. oracle foo = mlfun), additional name argument for invoke_oracle;
+
+* print_goals: optional output of const types (set show_consts and
+show_types);
 
 * improved output of warnings (###) / errors (***);
 
@@ -33,9 +43,6 @@
 * deleted the obsolete tactical STATE, which was declared by
     fun STATE tacfun st = tacfun st st;
 
-* slightly changed interfaces for oracles: admit many per theory, named
-(e.g. oracle foo = mlfun), additional name argument for invoke_oracle;
-
 
 *** Classical Reasoner ***