# HG changeset patch
# User haftmann
# Date 1274371248 -7200
# Node ID d754fb55a20fc2271c585910b9c176561b429b14
# Parent  a6e0696d7110e1ab7b1d8819d31ad09388f796be
proper code generator for complement

diff -r a6e0696d7110 -r d754fb55a20f src/HOL/Library/Dlist.thy
--- 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)