# HG changeset patch
# User wenzelm
# Date 935062960 -7200
# Node ID 9c7f17a259fc6bdf9c81f8d468174a9787fb3cba
# Parent  8cc10843475039ba1be76aa5f1d66b6955fbbb87
tuned;

diff -r 8cc108434750 -r 9c7f17a259fc NEWS
--- 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 ***