1.1 --- a/src/HOL/Complex.thy	Thu Oct 31 16:54:22 2013 +0100
     1.2 +++ b/src/HOL/Complex.thy	Fri Nov 01 18:51:14 2013 +0100
     1.3 @@ -587,7 +587,7 @@
     1.4    by (simp add: cis_def)
     1.5  
     1.6  lemma cis_divide: "cis a / cis b = cis (a - b)"
     1.7 -  by (simp add: complex_divide_def cis_mult diff_minus)
     1.8 +  by (simp add: complex_divide_def cis_mult)
     1.9  
    1.10  lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)"
    1.11    by (auto simp add: DeMoivre)