# HG changeset patch
# User wenzelm
# Date 1444146367 -7200
# Node ID b98cd131e2b5b9997b11ebda5b21d0475a7f1209
# Parent  e60c7d0bb4b17772610c53367ac341538d38f66b
isabelle update_cartouches;

diff -r e60c7d0bb4b1 -r b98cd131e2b5 src/HOL/Topological_Spaces.thy
--- 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