author | huffman |
Tue, 12 Dec 2006 07:11:58 +0100 | |
changeset 21785 | 885667874dfc |
parent 21784 | e76faa6e65fd |
child 21786 | 66da6af2b0c9 |
--- 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) \<noteq> 0 |] + shows "[| NSDERIV f x :> d; NSDERIV g x :> e; g(x) \<noteq> 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)