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