summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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"