src/HOL/Topological_Spaces.thy
changeset 60040 1fa1023b13b9
parent 60036 218fcc645d22
child 60150 bd773c47ad0b
     1.1 --- a/src/HOL/Topological_Spaces.thy	Sun Apr 12 11:33:50 2015 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Sun Apr 12 11:34:09 2015 +0200
     1.3 @@ -1636,7 +1636,7 @@
     1.4      by (rule compactE)
     1.5    from `D \<subseteq> ?C` have "\<forall>x\<in>D. eventually (\<lambda>y. y \<notin> x) (nhds y)" by auto
     1.6    with `finite D` have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
     1.7 -    by (simp add: eventually_Ball_finite)
     1.8 +    by (simp add: eventually_ball_finite)
     1.9    with `s \<subseteq> \<Union>D` have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
    1.10      by (auto elim!: eventually_mono [rotated])
    1.11    thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"