src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 59765 26d1c71784f1
parent 59587 8ea7b22525cb
child 59815 cce82e360c2f
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 20 14:06:15 2015 +0000
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 20 16:11:28 2015 +0000
     1.3 @@ -1250,7 +1250,7 @@
     1.4        e1 \<noteq> {} \<and>
     1.5        e2 \<noteq> {})"
     1.6    unfolding connected_def openin_open
     1.7 -  by blast
     1.8 +  by safe blast+
     1.9  
    1.10  lemma exists_diff:
    1.11    fixes P :: "'a set \<Rightarrow> bool"