# HG changeset patch
# User wenzelm
# Date 934992648 -7200
# Node ID a141985d660bdef9b03e79e021d207876dab7e59
# Parent  745f834281e2428ca3c1a6c0368623273ea690de
sum_case renamed to basic_sum_case;

diff -r 745f834281e2 -r a141985d660b 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 ***