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