| changeset 39198 | f967a16dfcdd |
| parent 37729 | daea77769276 |
| child 39302 | d7728f65b353 |
--- a/src/HOL/Library/FrechetDeriv.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/FrechetDeriv.thy Tue Sep 07 10:05:19 2010 +0200 @@ -177,7 +177,7 @@ hence "(\<lambda>h. F h - F' h) = (\<lambda>h. 0)" by (rule FDERIV_zero_unique) thus "F = F'" - unfolding expand_fun_eq right_minus_eq . + unfolding ext_iff right_minus_eq . qed subsection {* Continuity *}