src/HOL/Library/Countable_Set_Type.thy

     "(\<And>x. cin x A ==> P x) == Trueprop (cBall A (\<lambda>x. P x))"
 apply (simp only: atomize_all atomize_imp)
 apply (rule equal_intr_rule)
 by (transfer, simp)+
 
-subsubsection \<open>@{const cUnion}\<close>
+subsubsection \<open>\<^const>\<open>cUnion\<close>\<close>
 
 lemma cUNION_cimage: "cUNION (cimage f A) g = cUNION A (g \<circ> f)"
   by transfer simp