1.1 --- a/NEWS	Mon Feb 05 14:30:55 2001 +0100
     1.2 +++ b/NEWS	Mon Feb 05 14:31:49 2001 +0100
     1.3 @@ -2,6 +2,9 @@
     1.4  Isabelle NEWS -- history user-relevant changes
     1.5  ==============================================
     1.6  
     1.7 +New in Isabelle99-2 (February 2001)
     1.8 +-----------------------------------
     1.9 +
    1.10  *** Overview of INCOMPATIBILITIES ***
    1.11  
    1.12  * HOL: inductive package no longer splits induction rule aggressively,
    1.13 @@ -45,7 +48,7 @@
    1.14  like this: "A\<^sup>*" or "A\<^sup>\<star>";
    1.15  
    1.16  * some more standard symbols; see Appendix A of the system manual for
    1.17 -the complete list;
    1.18 +the complete list of symbols defined in isabellesym.sty;
    1.19  
    1.20  * improved isabelle style files; more abstract symbol implementation
    1.21  (should now use \isamath{...} and \isatext{...} in custom symbol
    1.22 @@ -56,11 +59,14 @@
    1.23  actual human-readable proof documents.  Please do not include goal
    1.24  states into document output unless you really know what you are doing!
    1.25  
    1.26 -* isatool unsymbolize tunes sources for plain ASCII communication;
    1.27 +* proper indentation of antiquoted output with proportional LaTeX
    1.28 +fonts;
    1.29  
    1.30  * no_document ML operator temporarily disables LaTeX document
    1.31  generation;
    1.32  
    1.33 +* isatool unsymbolize tunes sources for plain ASCII communication;
    1.34 +
    1.35  
    1.36  *** Isar ***
    1.37  
    1.38 @@ -159,7 +165,7 @@
    1.39  * print modes "brackets" and "no_brackets" control output of nested =>
    1.40  (types) and ==> (props); the default behaviour is "brackets";
    1.41  
    1.42 -* system: support Poly/ML 4.0 (current beta versions);
    1.43 +* system: support Poly/ML 4.0;
    1.44  
    1.45  * Pure: the Simplifier has been implemented properly as a derived rule
    1.46  outside of the actual kernel (at last!); the overall performance