diff -r 1c0805003c4f -r f0b5e6254a1f src/HOL/Hyperreal/Lim.thy --- a/src/HOL/Hyperreal/Lim.thy Wed Nov 01 17:14:16 2006 +0100 +++ b/src/HOL/Hyperreal/Lim.thy Wed Nov 01 17:57:02 2006 +0100 @@ -766,6 +766,15 @@ apply (blast intro: LIM_unique) done +text{*Differentiation of finite sum*} + +lemma DERIV_sumr [rule_format (no_asm)]: + "(\r. m \ r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) + --> DERIV (%x. \n=m.. (\r=m..