# HG changeset patch
# User nipkow
# Date 1288367856 -7200
# Node ID edec5213042bd36b9f2293bb6fdbeb3a1c7af260
# Parent  b12ae24459851ced225afbc228a0d5337b9b74a2
Plus -> Sum_Type.Plus

diff -r b12ae2445985 -r edec5213042b NEWS
--- a/NEWS	Fri Oct 29 17:28:27 2010 +0200
+++ b/NEWS	Fri Oct 29 17:57:36 2010 +0200
@@ -153,6 +153,9 @@
 * Abolished symbol type names:  "prod" and "sum" replace "*" and "+"
 respectively.  INCOMPATIBILITY.
 
+* Name "Plus" of disjoint sum operator "<+>" is now hidden.
+  Write Sum_Type.Plus.
+
 * Constant "split" has been merged with constant "prod_case";  names
 of ML functions, facts etc. involving split have been retained so far,
 though.  INCOMPATIBILITY.