1.1 --- a/src/HOL/Library/Dlist.thy	Thu May 20 17:35:02 2010 +0200
     1.2 +++ b/src/HOL/Library/Dlist.thy	Thu May 20 18:00:48 2010 +0200
     1.3 @@ -123,6 +123,8 @@
     1.4  declare UNIV_Set [code del]
     1.5  declare insert_Set [code del]
     1.6  declare remove_Set [code del]
     1.7 +declare compl_Set [code del]
     1.8 +declare compl_Coset [code del]
     1.9  declare map_Set [code del]
    1.10  declare filter_Set [code del]
    1.11  declare forall_Set [code del]
    1.12 @@ -185,6 +187,11 @@
    1.13    "Fset.member (Coset dxs) = Not \<circ> member dxs"
    1.14    by (simp_all add: member_def)
    1.15  
    1.16 +lemma compl_code [code]:
    1.17 +  "- Set dxs = Coset dxs"
    1.18 +  "- Coset dxs = Set dxs"
    1.19 +  by (simp_all add: not_set_compl member_set)
    1.20 +
    1.21  lemma map_code [code]:
    1.22    "Fset.map f (Set dxs) = Set (map f dxs)"
    1.23    by (simp add: member_set)