--- a/NEWS Thu Aug 19 13:39:26 1999 +0200
+++ b/NEWS Thu Aug 19 13:42:40 1999 +0200
@@ -178,9 +178,12 @@
All/Ex now support plain / symbolic / HOL notation; plain syntax for
Eps operator is provided as well: "SOME x. P[x]";
-* HOL/Sum: sum_case renamed to basic_sum_case; hardly an
+* HOL/Sum.thy: sum_case renamed to basic_sum_case; hardly an
INCOMPATIBILITY, users should refer to the version of HOL/Datatype;
+* HOL/Univ.thy: infix syntax <*>, <+>, <**>, <+> eliminated and made
+thus available for user theories;
+
*** LK ***