# HG changeset patch
# User wenzelm
# Date 878590619 -3600
# Node ID 1610602a2964a85ca8f2c8a2464f941e4ff34ca7
# Parent  2270829d23645a7fb5e8b37e847aae574045c7f3
isatool fixclasimp;

diff -r 2270829d2364 -r 1610602a2964 NEWS
--- a/NEWS	Mon Nov 03 21:15:08 1997 +0100
+++ b/NEWS	Mon Nov 03 21:56:59 1997 +0100
@@ -9,12 +9,18 @@
 
 * hierachically structured name spaces (for consts, types, axms,
 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 setting 'global_names' at compile time to disable
-qualified names for theories; may also fine tune theories via 'global'
-and 'local' section;
+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;
+
+* reimplemented the implicit simpset and claset using the new anytype
+data filed in signatures; references simpset:simpset ref etc. are
+replaced by functions simpset:unit->simpset and
+simpset_ref:unit->simpset ref; COMPATIBILITY: use isatool fixclasimp
+to patch your ML files accordingly;
 
 * HTML output now includes theory graph data for display with Java
 applet or isatool browser; data generated automatically via isatool