| changeset 44568 | e6f291cb5810 |
| parent 44282 | f0de18b62d63 |
| child 44575 | c5e42b8590dd |
--- a/src/HOL/Library/Product_Vector.thy Sat Aug 27 17:26:14 2011 +0200 +++ b/src/HOL/Library/Product_Vector.thy Sun Aug 28 09:20:12 2011 -0700 @@ -544,7 +544,7 @@ apply (rule FDERIV_bounded_linear [OF g]) apply (simp add: norm_Pair) apply (rule real_LIM_sandwich_zero) -apply (rule LIM_add_zero) +apply (rule tendsto_add_zero) apply (rule FDERIV_D [OF f]) apply (rule FDERIV_D [OF g]) apply (rename_tac h)