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.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.10  text {* Monotonicity in first argument *}
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)