# HG changeset patch
# User wenzelm
# Date 976224925 -3600
# Node ID b4c3af8ebada194ebd8c6f0621411cdb270fdab2
# Parent  85c5645a8a9346e37104fa9b277b8449e855f9c1
tuned;

diff -r 85c5645a8a93 -r b4c3af8ebada NEWS
--- 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