src/HOL/Complex.thy
changeset 37887 2ae085b07f2f
parent 37767 a2b7a20d6ea3
child 41959 b460124855b8
--- 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"