--- a/src/HOL/Topological_Spaces.thy Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Topological_Spaces.thy Sun Oct 21 09:39:09 2018 +0200
@@ -1882,7 +1882,7 @@
unfolding continuous_on_def
by (intro ball_cong filterlim_cong) (auto simp: eventually_at_filter)
-lemma continuous_on_strong_cong:
+lemma continuous_on_cong_strong:
"s = t \<Longrightarrow> (\<And>x. x \<in> t =simp=> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
unfolding simp_implies_def by (rule continuous_on_cong)