src/HOL/Complex.thy
changeset 53374 a14d2a854c02
parent 53015 a1119cf551e8
child 54230 b1d955791529
     1.1 --- a/src/HOL/Complex.thy	Tue Sep 03 00:51:08 2013 +0200
     1.2 +++ b/src/HOL/Complex.thy	Tue Sep 03 01:12:40 2013 +0200
     1.3 @@ -707,11 +707,11 @@
     1.4        unfolding d_def by simp
     1.5      moreover from a assms have "cos a = cos x" and "sin a = sin x"
     1.6        by (simp_all add: complex_eq_iff)
     1.7 -    hence "cos d = 1" unfolding d_def cos_diff by simp
     1.8 -    moreover hence "sin d = 0" by (rule cos_one_sin_zero)
     1.9 +    hence cos: "cos d = 1" unfolding d_def cos_diff by simp
    1.10 +    moreover from cos have "sin d = 0" by (rule cos_one_sin_zero)
    1.11      ultimately have "d = 0"
    1.12        unfolding sin_zero_iff even_mult_two_ex
    1.13 -      by (safe, auto simp add: numeral_2_eq_2 less_Suc_eq)
    1.14 +      by (auto simp add: numeral_2_eq_2 less_Suc_eq)
    1.15      thus "a = x" unfolding d_def by simp
    1.16    qed (simp add: assms del: Re_sgn Im_sgn)
    1.17    with `z \<noteq> 0` show "arg z = x"