src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 56073 29e308b56d23
parent 55927 30c41a8eca0e
child 56154 f0a927235162
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 12 22:57:50 2014 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Mar 13 07:07:07 2014 +0100
     1.3 @@ -2958,10 +2958,10 @@
     1.4    fix f
     1.5    assume *: "Ball f open" "s \<union> t \<subseteq> \<Union>f"
     1.6    from * `compact s` obtain s' where "s' \<subseteq> f \<and> finite s' \<and> s \<subseteq> \<Union>s'"
     1.7 -    unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f]) metis
     1.8 +    unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f])
     1.9    moreover
    1.10    from * `compact t` obtain t' where "t' \<subseteq> f \<and> finite t' \<and> t \<subseteq> \<Union>t'"
    1.11 -    unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f]) metis
    1.12 +    unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f])
    1.13    ultimately show "\<exists>f'\<subseteq>f. finite f' \<and> s \<union> t \<subseteq> \<Union>f'"
    1.14      by (auto intro!: exI[of _ "s' \<union> t'"])
    1.15  qed