changeset 7261 | a141985d660b |
parent 7252 | d3ed595dd772 |
child 7280 | 9c7f17a259fc |
--- 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 ***