--- a/NEWS Mon Jan 29 23:54:56 2001 +0100
+++ b/NEWS Tue Jan 30 14:21:50 2001 +0100
@@ -4,10 +4,8 @@
*** Overview of INCOMPATIBILITIES ***
-* HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse"
-operation;
-
-* HOL: induct renamed to lfp_induct;
+* HOL: induct renamed to lfp_induct, lfp_Tarski to lfp_unfold,
+gfp_Tarski to gfp_unfold;
* HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp;
@@ -15,6 +13,9 @@
relation); infix "^^" has been renamed "``"; infix "``" has been
renamed "`"; "univalent" has been renamed "single_valued";
+* HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse"
+operation;
+
* HOLCF: infix "`" has been renamed "$"; the symbol syntax is \<cdot>;
* Isar: 'obtain' no longer declares "that" fact as simp/intro;
@@ -29,10 +30,6 @@
*** Document preparation ***
-* improved isabelle style files; more abstract symbol implementation
-(should now use \isamath{...} and \isatext{...} in custom symbol
-definitions);
-
* \isabellestyle{NAME} selects version of Isabelle output (currently
available: are "it" for near math-mode best-style output, "sl" for
slanted text style, and "tt" for plain type-writer; if no
@@ -45,6 +42,10 @@
* some more standard symbols; see Appendix A of the system manual for
the complete list;
+* improved isabelle style files; more abstract symbol implementation
+(should now use \isamath{...} and \isatext{...} in custom symbol
+definitions);
+
* antiquotation @{goals} and @{subgoals} for output of *dynamic* goals
state; Note that presentation of goal states does not conform to
actual human-readable proof documents. Please do not include goal