changeset 72220 | bb29e4eb938d |
parent 72219 | 0f38c96a0a74 |
child 72980 | 4fc3dc37f406 |
--- a/src/HOL/Transcendental.thy Thu Aug 27 12:14:46 2020 +0100 +++ b/src/HOL/Transcendental.thy Thu Aug 27 15:23:48 2020 +0100 @@ -1003,7 +1003,7 @@ have *: "((\<lambda>x. if x = 0 then a 0 else f x) \<longlongrightarrow> a 0) (at 0)" by (rule powser_limit_0 [OF s]) (auto simp: powser_sums_zero sm) show ?thesis - using "*" by auto + using "*" by (auto cong: Lim_cong_within) qed