src/HOL/Analysis/Great_Picard.thy
changeset 65274 db2de50de28e
parent 65064 a4abec71279a
child 65823 4f353215888a
     1.1 --- a/src/HOL/Analysis/Great_Picard.thy	Thu Mar 16 13:55:29 2017 +0000
     1.2 +++ b/src/HOL/Analysis/Great_Picard.thy	Thu Mar 16 16:02:18 2017 +0000
     1.3 @@ -211,7 +211,7 @@
     1.4    have "\<exists>x. cos (complex_of_real pi * z) = of_int x"
     1.5      using assms
     1.6      apply safe
     1.7 -      apply (auto simp: Ints_def cos_exp_eq exp_minus)
     1.8 +      apply (auto simp: Ints_def cos_exp_eq exp_minus Complex_eq)
     1.9       apply (auto simp: algebra_simps dest: 1 2)
    1.10        done
    1.11    then have "sin(pi * cos(pi * z)) ^ 2 = 0"