src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 37452 8f515d6aded5
parent 36778 739a9379e29b
child 37486 b993fac7985b
child 37489 44e42d392c6e
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jun 17 16:15:15 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jun 17 19:32:05 2010 +0200
@@ -5266,7 +5266,7 @@
     (* class constraint due to continuous_on_inverse *)
   shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s
           \<Longrightarrow> s homeomorphic t"
-  unfolding homeomorphic_def by(metis homeomorphism_compact)
+  unfolding homeomorphic_def by (auto intro: homeomorphism_compact)
 
 text{* Preservation of topological properties.                                   *}