# 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;