changeset 46133 | d9fe85d3d2cd |
parent 45990 | b7b905b23b2a |
child 46146 | 6baea4fca6bd |
--- a/src/HOL/Library/Cset.thy Fri Jan 06 10:19:49 2012 +0100 +++ b/src/HOL/Library/Cset.thy Fri Jan 06 10:19:49 2012 +0100 @@ -370,7 +370,7 @@ lemma bind_set: "Cset.bind (Cset.set xs) f = fold (sup \<circ> f) xs (Cset.set [])" - by (simp add: Cset.bind_def SUPR_set_fold) + by (simp add: Cset.bind_def SUP_set_fold) hide_fact (open) bind_set lemma pred_of_cset_set: