src/HOL/Complex.thy
changeset 56238 5d147e1e18d1
parent 56217 dc429a5b13c4
child 56331 bea2196627cb
     1.1 --- a/src/HOL/Complex.thy	Fri Mar 21 08:13:23 2014 +0100
     1.2 +++ b/src/HOL/Complex.thy	Fri Mar 21 15:36:00 2014 +0000
     1.3 @@ -399,6 +399,10 @@
     1.4      by (rule convergentI)
     1.5  qed
     1.6  
     1.7 +declare
     1.8 +  DERIV_power[where 'a=complex, THEN DERIV_cong,
     1.9 +              unfolded of_nat_def[symmetric], DERIV_intros]
    1.10 +
    1.11  
    1.12  subsection {* The Complex Number $i$ *}
    1.13