src/HOL/Complex.thy
changeset 61649 268d88ec9087
parent 61609 77b453bd616f
child 61762 d50b993b4fb9
     1.1 --- a/src/HOL/Complex.thy	Thu Nov 12 11:22:26 2015 +0100
     1.2 +++ b/src/HOL/Complex.thy	Fri Nov 13 12:27:13 2015 +0000
     1.3 @@ -842,7 +842,7 @@
     1.4      by (simp add: cis_divide [symmetric] cis_2pi_int)
     1.5    moreover have "- pi < c \<and> c \<le> pi"
     1.6      using ceiling_correct [of "(b - pi) / (2*pi)"]
     1.7 -    by (simp add: c_def less_divide_eq divide_le_eq algebra_simps)
     1.8 +    by (simp add: c_def less_divide_eq divide_le_eq algebra_simps del: le_of_int_ceiling)
     1.9    ultimately show "\<exists>a. sgn z = cis a \<and> -pi < a \<and> a \<le> pi" by fast
    1.10  qed
    1.11