--- a/src/HOL/Topological_Spaces.thy Sun Dec 30 10:34:56 2018 +0000
+++ b/src/HOL/Topological_Spaces.thy Sun Dec 30 10:34:56 2018 +0000
@@ -1882,7 +1882,7 @@
unfolding continuous_on_def
by (intro ball_cong filterlim_cong) (auto simp: eventually_at_filter)
-lemma continuous_on_cong_strong:
+lemma continuous_on_cong_simp:
"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)