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