src/HOL/Library/Product_Vector.thy
changeset 49962 a8cc904a6820
parent 44749 5b1e1432c320
child 51002 496013a6eb38
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -421,7 +421,7 @@
     1.4    show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
     1.5      unfolding norm_prod_def
     1.6      apply (simp add: power_mult_distrib)
     1.7 -    apply (simp add: right_distrib [symmetric])
     1.8 +    apply (simp add: distrib_left [symmetric])
     1.9      apply (simp add: real_sqrt_mult_distrib)
    1.10      done
    1.11    show "sgn x = scaleR (inverse (norm x)) x"
    1.12 @@ -475,7 +475,7 @@
    1.13      apply (rule allI)
    1.14      apply (simp add: norm_Pair)
    1.15      apply (rule order_trans [OF sqrt_add_le_add_sqrt], simp, simp)
    1.16 -    apply (simp add: right_distrib)
    1.17 +    apply (simp add: distrib_left)
    1.18      apply (rule add_mono [OF norm_f norm_g])
    1.19      done
    1.20    then show "\<exists>K. \<forall>x. norm (f x, g x) \<le> norm x * K" ..
    1.21 @@ -528,7 +528,7 @@
    1.22      by (simp add: inner_add_left)
    1.23    show "inner (scaleR r x) y = r * inner x y"
    1.24      unfolding inner_prod_def
    1.25 -    by (simp add: right_distrib)
    1.26 +    by (simp add: distrib_left)
    1.27    show "0 \<le> inner x x"
    1.28      unfolding inner_prod_def
    1.29      by (intro add_nonneg_nonneg inner_ge_zero)