src/HOL/NthRoot.thy
changeset 57512 cc97b347b301
parent 57275 0ddb5b755cdc
child 57514 bdc2c6b40bf2
     1.1 --- a/src/HOL/NthRoot.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/NthRoot.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -222,7 +222,7 @@
     1.4             simp: sgn_zero_iff sgn_mult power_mult[symmetric] abs_mult power_mult_distrib abs_sgn_eq)
     1.5  
     1.6  lemma real_root_commute: "root m (root n x) = root n (root m x)"
     1.7 -  by (simp add: real_root_mult_exp [symmetric] mult_commute)
     1.8 +  by (simp add: real_root_mult_exp [symmetric] mult.commute)
     1.9  
    1.10  text {* Monotonicity in first argument *}
    1.11  
    1.12 @@ -432,7 +432,7 @@
    1.13    from n obtain m where m: "n = 2 * m"
    1.14      unfolding even_mult_two_ex ..
    1.15    from m have "sqrt (2 ^ n) = sqrt ((2 ^ m)\<^sup>2)"
    1.16 -    by (simp only: power_mult[symmetric] mult_commute)
    1.17 +    by (simp only: power_mult[symmetric] mult.commute)
    1.18    then show ?thesis
    1.19      using m by simp
    1.20  qed
    1.21 @@ -512,7 +512,7 @@
    1.22    proof (rule right_inverse_eq [THEN iffD1, THEN sym]) 
    1.23      show "sqrt x / x \<noteq> 0" by (simp add: divide_inverse nneg nz) 
    1.24      show "inverse (sqrt x) / (sqrt x / x) = 1"
    1.25 -      by (simp add: divide_inverse mult_assoc [symmetric] 
    1.26 +      by (simp add: divide_inverse mult.assoc [symmetric] 
    1.27                    power2_eq_square [symmetric] real_inv_sqrt_pow2 pos nz) 
    1.28    qed
    1.29  qed
    1.30 @@ -603,7 +603,7 @@
    1.31    "sqrt ((a + c)\<^sup>2 + (b + d)\<^sup>2) \<le> sqrt (a\<^sup>2 + b\<^sup>2) + sqrt (c\<^sup>2 + d\<^sup>2)"
    1.32  apply (rule power2_le_imp_le, simp)
    1.33  apply (simp add: power2_sum)
    1.34 -apply (simp only: mult_assoc distrib_left [symmetric])
    1.35 +apply (simp only: mult.assoc distrib_left [symmetric])
    1.36  apply (rule mult_left_mono)
    1.37  apply (rule power2_le_imp_le)
    1.38  apply (simp add: power2_sum power_mult_distrib)