--- a/src/HOL/Complex.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Complex.thy Mon Jul 19 16:09:44 2010 +0200
@@ -686,12 +686,12 @@
by (simp add: divide_inverse rcis_def)
lemma cis_divide: "cis a / cis b = cis (a - b)"
-by (simp add: complex_divide_def cis_mult diff_def)
+by (simp add: complex_divide_def cis_mult diff_minus)
lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
apply (simp add: complex_divide_def)
apply (case_tac "r2=0", simp)
-apply (simp add: rcis_inverse rcis_mult diff_def)
+apply (simp add: rcis_inverse rcis_mult diff_minus)
done
lemma Re_cis [simp]: "Re(cis a) = cos a"