src/HOL/Complex.thy
changeset 57512 cc97b347b301
parent 57259 3a448982a74a
child 58146 d91c1e50b36e
     1.1 --- a/src/HOL/Complex.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Complex.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4    show "scaleR (a + b) x = scaleR a x + scaleR b x"
     1.5      by (simp add: complex_eq_iff distrib_right)
     1.6    show "scaleR a (scaleR b x) = scaleR (a * b) x"
     1.7 -    by (simp add: complex_eq_iff mult_assoc)
     1.8 +    by (simp add: complex_eq_iff mult.assoc)
     1.9    show "scaleR 1 x = x"
    1.10      by (simp add: complex_eq_iff)
    1.11    show "scaleR a x * y = scaleR a (x * y)"
    1.12 @@ -190,7 +190,7 @@
    1.13    by (simp add: divide_complex_def)
    1.14  
    1.15  lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
    1.16 -  by (simp add: mult_assoc [symmetric])
    1.17 +  by (simp add: mult.assoc [symmetric])
    1.18  
    1.19  lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
    1.20    by (simp add: complex_eq_iff)
    1.21 @@ -298,14 +298,14 @@
    1.22    apply (rule abs_sqrt_wlog [where x="Re z"])
    1.23    apply (rule abs_sqrt_wlog [where x="Im z"])
    1.24    apply (rule power2_le_imp_le)
    1.25 -  apply (simp_all add: power2_sum add_commute sum_squares_bound real_sqrt_mult [symmetric])
    1.26 +  apply (simp_all add: power2_sum add.commute sum_squares_bound real_sqrt_mult [symmetric])
    1.27    done
    1.28  
    1.29  
    1.30  text {* Properties of complex signum. *}
    1.31  
    1.32  lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
    1.33 -  by (simp add: sgn_div_norm divide_inverse scaleR_conv_of_real mult_commute)
    1.34 +  by (simp add: sgn_div_norm divide_inverse scaleR_conv_of_real mult.commute)
    1.35  
    1.36  lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
    1.37    by (simp add: complex_sgn_def divide_inverse)
    1.38 @@ -703,7 +703,7 @@
    1.39  
    1.40  lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
    1.41  apply (insert rcis_Ex [of z])
    1.42 -apply (auto simp add: expi_def rcis_def mult_assoc [symmetric])
    1.43 +apply (auto simp add: expi_def rcis_def mult.assoc [symmetric])
    1.44  apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
    1.45  done
    1.46