src/HOL/Analysis/Convex_Euclidean_Space.thy

--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -346,7 +346,7 @@
 proof-
   have "{a..b} = {a..} \<inter> {..b}" by auto
   also have "interior \<dots> = {a<..} \<inter> {..<b}"
-    by (simp add: interior_real_atLeast interior_real_atMost)
+    by (simp)
   also have "\<dots> = {a<..<b}" by auto
   finally show ?thesis .
 qed