--- a/src/HOL/Library/Dlist.thy Thu May 20 17:35:02 2010 +0200
+++ b/src/HOL/Library/Dlist.thy Thu May 20 18:00:48 2010 +0200
@@ -123,6 +123,8 @@
declare UNIV_Set [code del]
declare insert_Set [code del]
declare remove_Set [code del]
+declare compl_Set [code del]
+declare compl_Coset [code del]
declare map_Set [code del]
declare filter_Set [code del]
declare forall_Set [code del]
@@ -185,6 +187,11 @@
"Fset.member (Coset dxs) = Not \<circ> member dxs"
by (simp_all add: member_def)
+lemma compl_code [code]:
+ "- Set dxs = Coset dxs"
+ "- Coset dxs = Set dxs"
+ by (simp_all add: not_set_compl member_set)
+
lemma map_code [code]:
"Fset.map f (Set dxs) = Set (map f dxs)"
by (simp add: member_set)