changeset 72220 | bb29e4eb938d |
parent 72219 | 0f38c96a0a74 |
child 72245 | cbe7aa1c2bdc |
--- a/src/HOL/Limits.thy Thu Aug 27 12:14:46 2020 +0100 +++ b/src/HOL/Limits.thy Thu Aug 27 15:23:48 2020 +0100 @@ -2178,7 +2178,7 @@ text \<open>A congruence rule allowing us to transform limits assuming not at point.\<close> -lemma Lim_cong_within [cong]: +lemma Lim_cong_within: assumes "a = b" and "x = y" and "S = T"