src/HOL/Complex.thy
changeset 37887 2ae085b07f2f
parent 37767 a2b7a20d6ea3
child 41959 b460124855b8
     1.1 --- a/src/HOL/Complex.thy	Mon Jul 19 16:09:44 2010 +0200
     1.2 +++ b/src/HOL/Complex.thy	Mon Jul 19 16:09:44 2010 +0200
     1.3 @@ -686,12 +686,12 @@
     1.4  by (simp add: divide_inverse rcis_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_def)
     1.8 +by (simp add: complex_divide_def cis_mult diff_minus)
     1.9  
    1.10  lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
    1.11  apply (simp add: complex_divide_def)
    1.12  apply (case_tac "r2=0", simp)
    1.13 -apply (simp add: rcis_inverse rcis_mult diff_def)
    1.14 +apply (simp add: rcis_inverse rcis_mult diff_minus)
    1.15  done
    1.16  
    1.17  lemma Re_cis [simp]: "Re(cis a) = cos a"