--- a/NEWS Mon Aug 23 11:43:21 1999 +0200
+++ b/NEWS Mon Aug 23 15:24:00 1999 +0200
@@ -183,8 +183,7 @@
All/Ex now support plain / symbolic / HOL notation; plain syntax for
Eps operator is provided as well: "SOME x. P[x]";
-* HOL/Sum.thy: sum_case renamed to basic_sum_case; hardly an
-INCOMPATIBILITY, users should refer to the version of HOL/Datatype;
+* HOL/Sum.thy: sum_case has been moved to HOL/Datatype;
* HOL/Univ.thy: infix syntax <*>, <+>, <**>, <+> eliminated and made
thus available for user theories;