merged
authornipkow
Sun, 31 Oct 2010 11:45:45 +0100
changeset 40541d4923a7f42c1
parent 40539 cd932ab8cb59
parent 40540 edec5213042b
child 40542 ac4d75f86d97
merged
NEWS
     1.1 --- a/NEWS	Sun Oct 31 11:38:09 2010 +0100
     1.2 +++ b/NEWS	Sun Oct 31 11:45:45 2010 +0100
     1.3 @@ -159,6 +159,9 @@
     1.4  * Abolished symbol type names:  "prod" and "sum" replace "*" and "+"
     1.5  respectively.  INCOMPATIBILITY.
     1.6  
     1.7 +* Name "Plus" of disjoint sum operator "<+>" is now hidden.
     1.8 +  Write Sum_Type.Plus.
     1.9 +
    1.10  * Constant "split" has been merged with constant "prod_case";  names
    1.11  of ML functions, facts etc. involving split have been retained so far,
    1.12  though.  INCOMPATIBILITY.