isabelle update_cartouches;
authorwenzelm
Tue Oct 06 17:46:07 2015 +0200 (2015-10-06)
changeset 61342b98cd131e2b5
parent 61341 e60c7d0bb4b1
child 61343 5b5656a63bd6
isabelle update_cartouches;
src/HOL/Topological_Spaces.thy
     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