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