diff -r d995733b635d -r f0de18b62d63 NEWS
--- a/NEWS	Thu Aug 18 17:42:35 2011 +0200
+++ b/NEWS	Thu Aug 18 13:36:58 2011 -0700
@@ -199,6 +199,19 @@
   tendsto_vector   ~> vec_tendstoI
   Cauchy_vector    ~> vec_CauchyI
 
+* Complex_Main: The locale interpretations for the bounded_linear and
+bounded_bilinear locales have been removed, in order to reduce the
+number of duplicate lemmas. Users must use the original names for
+distributivity theorems, potential INCOMPATIBILITY.
+
+  divide.add ~> add_divide_distrib
+  divide.diff ~> diff_divide_distrib
+  divide.setsum ~> setsum_divide_distrib
+  mult.add_right ~> right_distrib
+  mult.diff_right ~> right_diff_distrib
+  mult_right.setsum ~> setsum_right_distrib
+  mult_left.diff ~> left_diff_distrib
+
 
 *** Document preparation ***