# HG changeset patch
# User wenzelm
# Date 980860910 -3600
# Node ID fece8333adfc89131eadac267a9b7667257fe42d
# Parent  e14029f92770e900eedf9b30ca9dd6a57ba5547e
tuned;

diff -r e14029f92770 -r fece8333adfc NEWS
--- 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