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 \ 'a cset \ bool" is "op \" parametric member_transfer - .. + . lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer by (rule countable_empty) lift_definition cinsert :: "'a \ 'a cset \ 'a cset" is insert parametric Lifting_Set.insert_transfer