--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Apr 01 17:02:43 2019 +0100
@@ -879,7 +879,7 @@
"is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
unfolding is_interval_def by auto
-lemma is_interval_inter: "is_interval X \<Longrightarrow> is_interval Y \<Longrightarrow> is_interval (X \<inter> Y)"
+lemma is_interval_Int: "is_interval X \<Longrightarrow> is_interval Y \<Longrightarrow> is_interval (X \<inter> Y)"
unfolding is_interval_def
by blast