src/HOL/Library/Cardinality.thy
changeset 67443 3abf6a722518
parent 67399 eab6ce8368fa
child 68011 fb6469cdf094
--- a/src/HOL/Library/Cardinality.thy	Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/Library/Cardinality.thy	Tue Jan 16 09:30:00 2018 +0100
@@ -519,7 +519,7 @@
      (\<lambda>_. List.coset xs \<subseteq> set ys))"
 by simp
 
-notepad begin \<comment> "test code setup"
+notepad begin \<comment> \<open>test code setup\<close>
 have "List.coset [True] = set [False] \<and> 
       List.coset [] \<subseteq> List.set [True, False] \<and> 
       finite (List.coset [True])"