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) \<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)