--- a/NEWS Thu Dec 07 22:27:57 2000 +0100
+++ b/NEWS Thu Dec 07 22:35:25 2000 +0100
@@ -4,7 +4,8 @@
*** Overview of INCOMPATIBILITIES ***
-* HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" function;
+* HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse"
+function;
* HOL: induct renamed to lfp_induct;
@@ -26,10 +27,10 @@
* support sub/super scripts (for single symbols only), input syntax is
like this: "A\<^sup>*" or "A\<^sup>\<star>";
-* 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 states
-into document output unless you really know what you are doing!
+* 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
+states into document output unless you really know what you are doing!
*** Isar ***
@@ -88,6 +89,8 @@
*** General ***
+* system: support Poly/ML 4.0 (current beta versions);
+
* Pure: the Simplifier has been implemented properly as a derived rule
outside of the actual kernel (at last!); the overall performance
penalty in practical applications is about 50%, while reliability of