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