tuned;
authorwenzelm
Mon Dec 15 14:40:13 1997 +0100 (1997-12-15)
changeset 4410b68047c56fce
parent 4409 2af86fcb97d7
child 4411 345d2c67a5b5
tuned;
NEWS
src/Pure/ROOT.ML
     1.1 --- a/NEWS	Mon Dec 15 14:14:06 1997 +0100
     1.2 +++ b/NEWS	Mon Dec 15 14:40:13 1997 +0100
     1.3 @@ -2,8 +2,24 @@
     1.4  Isabelle NEWS -- history of user-visible changes
     1.5  ================================================
     1.6  
     1.7 -New in Isabelle???? (DATE ????)
     1.8 --------------------------------
     1.9 +New in Isabelle98 (January 1998)
    1.10 +--------------------------------
    1.11 +
    1.12 +*** Overview of INCOMPATIBILITIES (see below for more details) ***
    1.13 +
    1.14 +* changed lexical syntax of terms / types: dots made part of long
    1.15 +identifiers, e.g. "%x.x" no longer possible, should be "%x. x";
    1.16 +
    1.17 +* simpset (and claset) reference variable replaced by functions
    1.18 +simpset / simpset_ref;
    1.19 +
    1.20 +* no longer supports theory aliases (via merge) and non-trivial
    1.21 +implicit merge of thms' signatures;
    1.22 +
    1.23 +* most internal names of constants changed due to qualified names;
    1.24 +
    1.25 +* changed Pure/Sequence interface (see Pure/seq.ML);
    1.26 +
    1.27  
    1.28  *** General Changes ***
    1.29  
     2.1 --- a/src/Pure/ROOT.ML	Mon Dec 15 14:14:06 1997 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Mon Dec 15 14:40:13 1997 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4  *)
     2.5  
     2.6  val banner = "Pure Isabelle";
     2.7 -val version = "Isabelle98: Jan 1998";
     2.8 +val version = "Isabelle98: January 1998";
     2.9  
    2.10  print_depth 1;
    2.11