tuned;
authorwenzelm
Mon, 15 Dec 1997 14:40:13 +0100
changeset 4410 b68047c56fce
parent 4409 2af86fcb97d7
child 4411 345d2c67a5b5
tuned;
NEWS
src/Pure/ROOT.ML
--- a/NEWS	Mon Dec 15 14:14:06 1997 +0100
+++ b/NEWS	Mon Dec 15 14:40:13 1997 +0100
@@ -2,8 +2,24 @@
 Isabelle NEWS -- history of user-visible changes
 ================================================
 
-New in Isabelle???? (DATE ????)
--------------------------------
+New in Isabelle98 (January 1998)
+--------------------------------
+
+*** Overview of INCOMPATIBILITIES (see below for more details) ***
+
+* changed lexical syntax of terms / types: dots made part of long
+identifiers, e.g. "%x.x" no longer possible, should be "%x. x";
+
+* simpset (and claset) reference variable replaced by functions
+simpset / simpset_ref;
+
+* no longer supports theory aliases (via merge) and non-trivial
+implicit merge of thms' signatures;
+
+* most internal names of constants changed due to qualified names;
+
+* changed Pure/Sequence interface (see Pure/seq.ML);
+
 
 *** General Changes ***
 
--- a/src/Pure/ROOT.ML	Mon Dec 15 14:14:06 1997 +0100
+++ b/src/Pure/ROOT.ML	Mon Dec 15 14:40:13 1997 +0100
@@ -8,7 +8,7 @@
 *)
 
 val banner = "Pure Isabelle";
-val version = "Isabelle98: Jan 1998";
+val version = "Isabelle98: January 1998";
 
 print_depth 1;