src/HOL/Limits.thy
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"