src/HOL/Library/Countable_Set_Type.thy

   acset_inverse[Transfer.transferred, unfolded mem_Collect_eq, simp]
   acset_inject[Transfer.transferred, unfolded mem_Collect_eq, simp]
   rcset[Transfer.transferred, unfolded mem_Collect_eq, simp]
 
 lift_definition cin :: "'a \<Rightarrow> 'a cset \<Rightarrow> bool" is "op \<in>" parametric member_transfer
-  ..
+  .
 lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer
   by (rule countable_empty)
 lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric Lifting_Set.insert_transfer
   by (rule countable_insert)
 lift_definition csingle :: "'a \<Rightarrow> 'a cset" is "\<lambda>x. {x}"