diff -r e76faa6e65fd -r 885667874dfc src/HOL/Hyperreal/Deriv.thy --- a/src/HOL/Hyperreal/Deriv.thy Tue Dec 12 04:37:25 2006 +0100 +++ b/src/HOL/Hyperreal/Deriv.thy Tue Dec 12 07:11:58 2006 +0100 @@ -699,7 +699,7 @@ lemma NSDERIV_quotient: fixes x :: "'a::{real_normed_field,recpower}" - shows "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \ 0 |] + shows "[| NSDERIV f x :> d; NSDERIV g x :> e; g(x) \ 0 |] ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))" by (simp add: NSDERIV_DERIV_iff DERIV_quotient del: realpow_Suc)