sum_case renamed to basic_sum_case;
authorwenzelm
Wed, 18 Aug 1999 18:10:48 +0200
changeset 7261 a141985d660b
parent 7260 745f834281e2
child 7262 a05dc63ca29b
sum_case renamed to basic_sum_case;
NEWS
--- 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 ***