src/ZF/ex/Ramsey.thy

--- a/src/ZF/ex/Ramsey.thy	Tue Jan 16 09:12:16 2018 +0100
+++ b/src/ZF/ex/Ramsey.thy	Tue Jan 16 09:30:00 2018 +0100
@@ -31,7 +31,7 @@
     "Symmetric(E) == (\<forall>x y. <x,y>:E \<longrightarrow> <y,x>:E)"
 
 definition
-  Atleast :: "[i,i]=>o" where \<comment> "not really necessary: ZF defines cardinality"
+  Atleast :: "[i,i]=>o" where \<comment> \<open>not really necessary: ZF defines cardinality\<close>
     "Atleast(n,S) == (\<exists>f. f \<in> inj(n,S))"
 
 definition