src/HOL/Real_Vector_Spaces.thy
changeset 57514 bdc2c6b40bf2
parent 57512 cc97b347b301
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sat Jul 05 10:09:01 2014 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Sat Jul 05 11:01:53 2014 +0200
     1.3 @@ -897,7 +897,7 @@
     1.4    also have "norm ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) \<le> (\<Sum>i\<in>I. norm (z i - w i))"
     1.5      using insert by auto
     1.6    finally show ?case
     1.7 -    by (auto simp add: add_ac mult_right_mono mult_left_mono)
     1.8 +    by (auto simp add: ac_simps mult_right_mono mult_left_mono)
     1.9  qed simp_all
    1.10  
    1.11  lemma norm_power_diff: 
    1.12 @@ -1159,7 +1159,7 @@
    1.13  
    1.14  lemma sgn_scaleR:
    1.15    "sgn (scaleR r x) = scaleR (sgn r) (sgn(x::'a::real_normed_vector))"
    1.16 -by (simp add: sgn_div_norm mult_ac)
    1.17 +by (simp add: sgn_div_norm ac_simps)
    1.18  
    1.19  lemma sgn_one [simp]: "sgn (1::'a::real_normed_algebra_1) = 1"
    1.20  by (simp add: sgn_div_norm)
    1.21 @@ -1308,7 +1308,7 @@
    1.22  apply (rule_tac K="norm b * K" in bounded_linear_intro)
    1.23  apply (rule add_left)
    1.24  apply (rule scaleR_left)
    1.25 -apply (simp add: mult_ac)
    1.26 +apply (simp add: ac_simps)
    1.27  done
    1.28  
    1.29  lemma bounded_linear_right:
    1.30 @@ -1317,7 +1317,7 @@
    1.31  apply (rule_tac K="norm a * K" in bounded_linear_intro)
    1.32  apply (rule add_right)
    1.33  apply (rule scaleR_right)
    1.34 -apply (simp add: mult_ac)
    1.35 +apply (simp add: ac_simps)
    1.36  done
    1.37  
    1.38  lemma prod_diff_prod: