src/HOL/Lifting_Set.thy
changeset 53952 b2781a3ce958
parent 53945 4191acef9d0e
child 54257 5c7a3b6b05a9
     1.1 --- a/src/HOL/Lifting_Set.thy	Fri Sep 27 14:43:26 2013 +0200
     1.2 +++ b/src/HOL/Lifting_Set.thy	Fri Sep 27 14:43:26 2013 +0200
     1.3 @@ -162,6 +162,10 @@
     1.4      by(rule SUPR_eq)(auto 4 4 dest: set_relD1[OF AB] set_relD2[OF AB] fun_relD[OF fg] intro: rev_bexI)
     1.5  qed
     1.6  
     1.7 +lemma bind_transfer [transfer_rule]:
     1.8 +  "(set_rel A ===> (A ===> set_rel B) ===> set_rel B) Set.bind Set.bind"
     1.9 +unfolding bind_UNION[abs_def] by transfer_prover
    1.10 +
    1.11  subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *}
    1.12  
    1.13  lemma member_transfer [transfer_rule]: