| changeset 44560 | 1711be44e76a |
| parent 44558 | cc878a312673 |
| child 45969 | 562e99c3d316 |
--- a/src/HOL/Library/List_Cset.thy Sat Aug 27 19:52:58 2011 +0200 +++ b/src/HOL/Library/List_Cset.thy Sun Aug 28 08:12:54 2011 +0200 @@ -64,7 +64,7 @@ declare compl_set [code] declare compl_coset [code] -declare subtract_remove [cpde] +declare subtract_remove [code] lemma map_set [code]: "Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"