# HG changeset patch
# User wenzelm
# Date 1468574796 -7200
# Node ID b0f8845e349895e843530ce915e93a7c0911fefb
# Parent  ac0a3b9c6dae9a8c60a7e99034789c511d326500
proper latex;

diff -r ac0a3b9c6dae -r b0f8845e3498 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Fri Jul 15 11:07:51 2016 +0200
+++ b/src/HOL/Topological_Spaces.thy	Fri Jul 15 11:26:36 2016 +0200
@@ -1942,7 +1942,8 @@
   by (simp add: continuous_within filterlim_at_split)
 
 text \<open>
-  The following open/closed Collect lemmas are ported from Sébastien Gouëzel's Ergodic_Theory.
+  The following open/closed Collect lemmas are ported from
+  Sébastien Gouëzel's \<open>Ergodic_Theory\<close>.
 \<close>
 lemma open_Collect_neq:
   fixes f g :: "'a::topological_space \<Rightarrow> 'b::t2_space"