--- a/src/HOL/Library/Countable_Set_Type.thy Tue Feb 18 23:03:49 2014 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy Tue Feb 18 23:03:50 2014 +0100
@@ -69,7 +69,7 @@
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