NEWS
changeset 7261 a141985d660b
parent 7252 d3ed595dd772
child 7280 9c7f17a259fc
--- a/NEWS	Wed Aug 18 17:43:53 1999 +0200
+++ b/NEWS	Wed Aug 18 18:10:48 1999 +0200
@@ -178,6 +178,9 @@
 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
+INCOMPATIBILITY, users should refer to the version of HOL/Datatype;
+
 
 *** LK ***