1.1 --- a/src/HOL/Complex.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/Complex.thy	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -141,7 +141,7 @@
     1.4  
     1.5  instance
     1.6    by intro_classes (simp_all add: complex_mult_def
     1.7 -    right_distrib left_distrib right_diff_distrib left_diff_distrib
     1.8 +    distrib_left distrib_right right_diff_distrib left_diff_distrib
     1.9      complex_inverse_def complex_divide_def
    1.10      power2_eq_square add_divide_distrib [symmetric]
    1.11      complex_eq_iff)
    1.12 @@ -206,9 +206,9 @@
    1.13  proof
    1.14    fix a b :: real and x y :: complex
    1.15    show "scaleR a (x + y) = scaleR a x + scaleR a y"
    1.16 -    by (simp add: complex_eq_iff right_distrib)
    1.17 +    by (simp add: complex_eq_iff distrib_left)
    1.18    show "scaleR (a + b) x = scaleR a x + scaleR b x"
    1.19 -    by (simp add: complex_eq_iff left_distrib)
    1.20 +    by (simp add: complex_eq_iff distrib_right)
    1.21    show "scaleR a (scaleR b x) = scaleR (a * b) x"
    1.22      by (simp add: complex_eq_iff mult_assoc)
    1.23    show "scaleR 1 x = x"
    1.24 @@ -297,7 +297,7 @@
    1.25         (simp add: real_sqrt_sum_squares_triangle_ineq)
    1.26    show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
    1.27      by (induct x)
    1.28 -       (simp add: power_mult_distrib right_distrib [symmetric] real_sqrt_mult)
    1.29 +       (simp add: power_mult_distrib distrib_left [symmetric] real_sqrt_mult)
    1.30    show "norm (x * y) = norm x * norm y"
    1.31      by (induct x, induct y)
    1.32         (simp add: real_sqrt_mult [symmetric] power2_eq_square algebra_simps)
    1.33 @@ -730,7 +730,7 @@
    1.34      unfolding z b_def rcis_def using `r \<noteq> 0`
    1.35      by (simp add: of_real_def sgn_scaleR sgn_if, simp add: cis_def)
    1.36    have cis_2pi_nat: "\<And>n. cis (2 * pi * real_of_nat n) = 1"
    1.37 -    by (induct_tac n, simp_all add: right_distrib cis_mult [symmetric],
    1.38 +    by (induct_tac n, simp_all add: distrib_left cis_mult [symmetric],
    1.39        simp add: cis_def)
    1.40    have cis_2pi_int: "\<And>x. cis (2 * pi * real_of_int x) = 1"
    1.41      by (case_tac x rule: int_diff_cases,