1.1 --- a/src/HOL/Library/Inner_Product.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/Library/Inner_Product.thy	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -201,7 +201,7 @@
     1.4    show "inner x y = inner y x"
     1.5      unfolding inner_real_def by (rule mult_commute)
     1.6    show "inner (x + y) z = inner x z + inner y z"
     1.7 -    unfolding inner_real_def by (rule left_distrib)
     1.8 +    unfolding inner_real_def by (rule distrib_right)
     1.9    show "inner (scaleR r x) y = r * inner x y"
    1.10      unfolding inner_real_def real_scaleR_def by (rule mult_assoc)
    1.11    show "0 \<le> inner x x"
    1.12 @@ -225,9 +225,9 @@
    1.13    show "inner x y = inner y x"
    1.14      unfolding inner_complex_def by (simp add: mult_commute)
    1.15    show "inner (x + y) z = inner x z + inner y z"
    1.16 -    unfolding inner_complex_def by (simp add: left_distrib)
    1.17 +    unfolding inner_complex_def by (simp add: distrib_right)
    1.18    show "inner (scaleR r x) y = r * inner x y"
    1.19 -    unfolding inner_complex_def by (simp add: right_distrib)
    1.20 +    unfolding inner_complex_def by (simp add: distrib_left)
    1.21    show "0 \<le> inner x x"
    1.22      unfolding inner_complex_def by simp
    1.23    show "inner x x = 0 \<longleftrightarrow> x = 0"