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])"