src/HOL/Analysis/Inner_Product.thy
changeset 68611 4bc4b5c0ccfc
parent 68499 d4312962161a
child 68617 75129a73aca3
     1.1 --- a/src/HOL/Analysis/Inner_Product.thy	Tue Jul 10 09:52:22 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Tue Jul 10 23:18:08 2018 +0100
     1.3 @@ -153,7 +153,7 @@
     1.4          unfolding norm_eq_sqrt_inner by simp
     1.5      qed
     1.6    have "sqrt (a\<^sup>2 * inner x x) = \<bar>a\<bar> * sqrt (inner x x)"
     1.7 -    by (simp add: real_sqrt_mult_distrib)
     1.8 +    by (simp add: real_sqrt_mult)
     1.9    then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
    1.10      unfolding norm_eq_sqrt_inner
    1.11      by (simp add: power2_eq_square mult.assoc)