src/HOL/Library/Dlist_Cset.thy
changeset 44563 01b2732cf4ad
parent 44558 cc878a312673
child 47232 e2f0176149d0
--- a/src/HOL/Library/Dlist_Cset.thy	Sun Aug 28 08:13:58 2011 +0200
+++ b/src/HOL/Library/Dlist_Cset.thy	Sun Aug 28 08:43:25 2011 +0200
@@ -118,7 +118,7 @@
 
 end
 
-declare Cset.single_code[code]
+declare Cset.single_code [code]
 
 lemma bind_set [code]:
   "Cset.bind (Dlist_Cset.Set xs) f = fold (sup \<circ> f) (list_of_dlist xs) Cset.empty"
@@ -130,6 +130,4 @@
   by (simp add: Cset.pred_of_cset_set Dlist_Cset.Set_def)
 hide_fact (open) pred_of_cset_set
 
-export_code "Cset._" in Haskell
-
 end