1.1 --- a/NEWS	Mon Jan 29 23:54:56 2001 +0100
     1.2 +++ b/NEWS	Tue Jan 30 14:21:50 2001 +0100
     1.3 @@ -4,10 +4,8 @@
     1.4  
     1.5  *** Overview of INCOMPATIBILITIES ***
     1.6  
     1.7 -* HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse"
     1.8 -operation;
     1.9 -
    1.10 -* HOL: induct renamed to lfp_induct;
    1.11 +* HOL: induct renamed to lfp_induct, lfp_Tarski to lfp_unfold,
    1.12 +gfp_Tarski to gfp_unfold;
    1.13  
    1.14  * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp;
    1.15  
    1.16 @@ -15,6 +13,9 @@
    1.17  relation); infix "^^" has been renamed "``"; infix "``" has been
    1.18  renamed "`"; "univalent" has been renamed "single_valued";
    1.19  
    1.20 +* HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse"
    1.21 +operation;
    1.22 +
    1.23  * HOLCF: infix "`" has been renamed "$"; the symbol syntax is \<cdot>;
    1.24  
    1.25  * Isar: 'obtain' no longer declares "that" fact as simp/intro;
    1.26 @@ -29,10 +30,6 @@
    1.27  
    1.28  *** Document preparation ***
    1.29  
    1.30 -* improved isabelle style files; more abstract symbol implementation
    1.31 -(should now use \isamath{...} and \isatext{...} in custom symbol
    1.32 -definitions);
    1.33 -
    1.34  * \isabellestyle{NAME} selects version of Isabelle output (currently
    1.35  available: are "it" for near math-mode best-style output, "sl" for
    1.36  slanted text style, and "tt" for plain type-writer; if no
    1.37 @@ -45,6 +42,10 @@
    1.38  * some more standard symbols; see Appendix A of the system manual for
    1.39  the complete list;
    1.40  
    1.41 +* improved isabelle style files; more abstract symbol implementation
    1.42 +(should now use \isamath{...} and \isatext{...} in custom symbol
    1.43 +definitions);
    1.44 +
    1.45  * antiquotation @{goals} and @{subgoals} for output of *dynamic* goals
    1.46  state; Note that presentation of goal states does not conform to
    1.47  actual human-readable proof documents.  Please do not include goal