src/HOL/Library/Quotient_Set.thy
changeset 47922 bba52dffab2b
parent 47777 f29e7dcd7c40
child 47936 756f30eac792
     1.1 --- a/src/HOL/Library/Quotient_Set.thy	Mon May 14 15:54:26 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Set.thy	Mon May 14 17:09:11 2012 +0200
     1.3 @@ -112,6 +112,11 @@
     1.4    apply (simp add: set_rel_def, fast)
     1.5    done
     1.6  
     1.7 +lemma set_rel_transfer [transfer_rule]:
     1.8 +  "((A ===> B ===> op =) ===> set_rel A ===> set_rel B ===> op =)
     1.9 +    set_rel set_rel"
    1.10 +  unfolding fun_rel_def set_rel_def by fast
    1.11 +
    1.12  subsubsection {* Rules requiring bi-unique or bi-total relations *}
    1.13  
    1.14  lemma member_transfer [transfer_rule]: