src/HOL/Library/Product_Vector.thy

     apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq])
     apply (simp add: add_mono power_mono norm_triangle_ineq)
     done
   show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
     unfolding norm_prod_def
-    apply (simp add: norm_scaleR power_mult_distrib)
+    apply (simp add: power_mult_distrib)
     apply (simp add: right_distrib [symmetric])
     apply (simp add: real_sqrt_mult_distrib)
     done
   show "sgn x = scaleR (inverse (norm x)) x"
     by (rule sgn_prod_def)