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
```