src/HOL/Deriv.thy

--- a/src/HOL/Deriv.thy	Fri Mar 07 14:21:15 2014 +0100
+++ b/src/HOL/Deriv.thy	Fri Mar 07 15:52:56 2014 +0000
@@ -790,7 +790,7 @@
 
 text {* Caratheodory formulation of derivative at a point *}
 
-lemma CARAT_DERIV:
+lemma CARAT_DERIV: (*FIXME: SUPERSEDED BY THE ONE IN Deriv.thy. But still used by NSA/HDeriv.thy*)
   "(DERIV f x :> l) \<longleftrightarrow> (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isCont g x \<and> g x = l)"
       (is "?lhs = ?rhs")
 proof