equal
deleted
inserted
replaced
138 |
138 |
139 lemma CDERIV_pow [simp]: |
139 lemma CDERIV_pow [simp]: |
140 "DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))" |
140 "DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))" |
141 apply (induct n) |
141 apply (induct n) |
142 apply (drule_tac [2] DERIV_ident [THEN DERIV_mult]) |
142 apply (drule_tac [2] DERIV_ident [THEN DERIV_mult]) |
143 apply (auto simp add: left_distrib real_of_nat_Suc) |
143 apply (auto simp add: distrib_right real_of_nat_Suc) |
144 apply (case_tac "n") |
144 apply (case_tac "n") |
145 apply (auto simp add: mult_ac add_commute) |
145 apply (auto simp add: mult_ac add_commute) |
146 done |
146 done |
147 |
147 |
148 text{*Nonstandard version*} |
148 text{*Nonstandard version*} |