NEWS
changeset 7320 e89fd7d0a624
parent 7313 300487ddfba9
child 7324 6cb0d0202298
     1.1 --- a/NEWS	Mon Aug 23 11:43:21 1999 +0200
     1.2 +++ b/NEWS	Mon Aug 23 15:24:00 1999 +0200
     1.3 @@ -183,8 +183,7 @@
     1.4  All/Ex now support plain / symbolic / HOL notation; plain syntax for
     1.5  Eps operator is provided as well: "SOME x. P[x]";
     1.6  
     1.7 -* HOL/Sum.thy: sum_case renamed to basic_sum_case; hardly an
     1.8 -INCOMPATIBILITY, users should refer to the version of HOL/Datatype;
     1.9 +* HOL/Sum.thy: sum_case has been moved to HOL/Datatype;
    1.10  
    1.11  * HOL/Univ.thy: infix syntax <*>, <+>, <**>, <+> eliminated and made
    1.12  thus available for user theories;