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
```