src/HOL/Deriv.thy
changeset 68644 242d298526a3
parent 68638 87d1bff264df
child 69020 4f94e262976d
     1.1 --- a/src/HOL/Deriv.thy	Sun Jul 15 21:58:50 2018 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Mon Jul 16 23:33:28 2018 +0100
     1.3 @@ -1086,7 +1086,7 @@
     1.4  
     1.5  text \<open>Caratheodory formulation of derivative at a point\<close>
     1.6  
     1.7 -lemma CARAT_DERIV: (*FIXME: SUPERSEDED BY THE ONE IN Deriv.thy. But still used by NSA/HDeriv.thy*)
     1.8 +lemma CARAT_DERIV:
     1.9    "(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)"
    1.10    (is "?lhs = ?rhs")
    1.11  proof
    1.12 @@ -1103,8 +1103,6 @@
    1.13    qed
    1.14  next
    1.15    assume ?rhs
    1.16 -  then obtain g where "(\<forall>z. f z - f x = g z * (z - x))" and "isCont g x" and "g x = l"
    1.17 -    by blast
    1.18    then show ?lhs
    1.19      by (auto simp add: isCont_iff DERIV_def cong: LIM_cong)
    1.20  qed