src/HOL/Topological_Spaces.thy
changeset 61342 b98cd131e2b5
parent 61306 9dd394c866fc
child 61426 d53db136e8fd
     1.1 --- a/src/HOL/Topological_Spaces.thy	Tue Oct 06 17:44:32 2015 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Oct 06 17:46:07 2015 +0200
     1.3 @@ -1867,7 +1867,7 @@
     1.4    obtain x where x: "\<And>s. s \<in> S \<Longrightarrow> x \<in> s"
     1.5      using ne by auto
     1.6    then have "x \<in> \<Union>S"
     1.7 -    using `sa \<in> S` by blast
     1.8 +    using \<open>sa \<in> S\<close> by blast
     1.9    then have "x \<in> A \<or> x \<in> B"
    1.10      using cover by auto
    1.11    then show False