
diff -r e81ee43ab290 -r f663fc1e653b src/HOL/Library/Countable_Set_Type.thy
--- 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




