# HG changeset patch
# User berghofe
# Date 935414640 -7200
# Node ID e89fd7d0a6249a4ffabb4ee22a60899ac1ee3eab
# Parent  3907d597cae617f6c8a68897e2ad7c13c125810a
Moved sum_case to theory HOL/Datatype.

diff -r 3907d597cae6 -r e89fd7d0a624 NEWS
--- a/NEWS	Mon Aug 23 11:43:21 1999 +0200
+++ b/NEWS	Mon Aug 23 15:24:00 1999 +0200
@@ -183,8 +183,7 @@
 All/Ex now support plain / symbolic / HOL notation; plain syntax for
 Eps operator is provided as well: "SOME x. P[x]";
 
-* HOL/Sum.thy: sum_case renamed to basic_sum_case; hardly an
-INCOMPATIBILITY, users should refer to the version of HOL/Datatype;
+* HOL/Sum.thy: sum_case has been moved to HOL/Datatype;
 
 * HOL/Univ.thy: infix syntax <*>, <+>, <**>, <+> eliminated and made
 thus available for user theories;