src/HOL/Complex.thy
changeset 56479 91958d4b30f7
parent 56409 36489d77c484
child 56541 0e3abadbef39
     1.1 --- a/src/HOL/Complex.thy	Tue Apr 08 23:16:00 2014 +0200
     1.2 +++ b/src/HOL/Complex.thy	Wed Apr 09 09:37:47 2014 +0200
     1.3 @@ -145,7 +145,7 @@
     1.4    by (simp add: complex_inverse_def)
     1.5  
     1.6  instance
     1.7 -  by intro_classes (simp_all add: complex_mult_def divide_minus_left
     1.8 +  by intro_classes (simp_all add: complex_mult_def
     1.9      distrib_left distrib_right right_diff_distrib left_diff_distrib
    1.10      complex_inverse_def complex_divide_def
    1.11      power2_eq_square add_divide_distrib [symmetric]
    1.12 @@ -656,7 +656,7 @@
    1.13      moreover have "!!u v. u / (x\<^sup>2 + y\<^sup>2) + v / (x\<^sup>2 + y\<^sup>2) = (u + v) / (x\<^sup>2 + y\<^sup>2)"
    1.14        by (metis add_divide_distrib)
    1.15      ultimately show ?thesis using Complex False `0 < x\<^sup>2 + y\<^sup>2`
    1.16 -      apply (simp add: complex_divide_def divide_minus_left zero_less_divide_iff less_divide_eq)
    1.17 +      apply (simp add: complex_divide_def  zero_less_divide_iff less_divide_eq)
    1.18        apply (metis less_divide_eq mult_zero_left diff_conv_add_uminus minus_divide_left)
    1.19        done
    1.20    qed
    1.21 @@ -844,7 +844,7 @@
    1.22      real (fact n) *\<^sub>R Complex (cos_coeff n * b ^ n) (sin_coeff n * b ^ n)"
    1.23        apply (induct n)
    1.24        apply (simp add: cos_coeff_def sin_coeff_def)
    1.25 -      apply (simp add: sin_coeff_Suc cos_coeff_Suc divide_minus_left del: mult_Suc)
    1.26 +      apply (simp add: sin_coeff_Suc cos_coeff_Suc del: mult_Suc)
    1.27        done } note * = this
    1.28    show "Re (cis b) = Re (exp (Complex 0 b))"
    1.29      unfolding exp_def cis_def cos_def