src/HOL/Library/Cardinality.thy

 
 class card_UNIV = finite_UNIV +
   fixes card_UNIV :: "'a card_UNIV"
   assumes card_UNIV: "card_UNIV = Phantom('a) CARD('a)"
 
-subsection \<open>Instantiations for @{text "card_UNIV"}\<close>
+subsection \<open>Instantiations for \<open>card_UNIV\<close>\<close>
 
 instantiation nat :: card_UNIV begin
 definition "finite_UNIV = Phantom(nat) False"
 definition "card_UNIV = Phantom(nat) 0"
 instance by intro_classes (simp_all add: finite_UNIV_nat_def card_UNIV_nat_def)

    else Code.abort
      (STR ''subset_eq (List.coset _) (List.set _) requires type class instance card_UNIV'')
      (\<lambda>_. List.coset xs \<subseteq> set ys))"
 by simp
 
-notepad begin -- "test code setup"
+notepad begin \<comment> "test code setup"
 have "List.coset [True] = set [False] \<and> 
       List.coset [] \<subseteq> List.set [True, False] \<and> 
       finite (List.coset [True])"
   by eval
 end