--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Sun May 20 18:37:34 2018 +0100
@@ -250,8 +250,8 @@
lemma homeomorphic_closed_intervals_real:
fixes a::real and b and c::real and d
assumes "a<b" and "c<d"
- shows "{a..b} homeomorphic {c..d}"
-by (metis assms compact_interval continuous_on_id convex_real_interval(5) emptyE homeomorphic_convex_compact interior_atLeastAtMost_real mvt)
+ shows "{a..b} homeomorphic {c..d}"
+ using assms by (auto intro: homeomorphic_convex_compact)
no_notation
eucl_less (infix "<e" 50)