Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
isabelle update_cartouches;
authorwenzelm
Tue, 06 Oct 2015 17:46:07 +0200
changeset 61342 b98cd131e2b5
parent 61341 e60c7d0bb4b1
child 61343 5b5656a63bd6
isabelle update_cartouches;
src/HOL/Topological_Spaces.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle