1.1 --- a/NEWS	Thu Aug 18 17:42:35 2011 +0200
     1.2 +++ b/NEWS	Thu Aug 18 13:36:58 2011 -0700
     1.3 @@ -199,6 +199,19 @@
     1.4    tendsto_vector   ~> vec_tendstoI
     1.5    Cauchy_vector    ~> vec_CauchyI
     1.6  
     1.7 +* Complex_Main: The locale interpretations for the bounded_linear and
     1.8 +bounded_bilinear locales have been removed, in order to reduce the
     1.9 +number of duplicate lemmas. Users must use the original names for
    1.10 +distributivity theorems, potential INCOMPATIBILITY.
    1.11 +
    1.12 +  divide.add ~> add_divide_distrib
    1.13 +  divide.diff ~> diff_divide_distrib
    1.14 +  divide.setsum ~> setsum_divide_distrib
    1.15 +  mult.add_right ~> right_distrib
    1.16 +  mult.diff_right ~> right_diff_distrib
    1.17 +  mult_right.setsum ~> setsum_right_distrib
    1.18 +  mult_left.diff ~> left_diff_distrib
    1.19 +
    1.20  
    1.21  *** Document preparation ***
    1.22