src/HOL/Library/Quotient_Sum.thy
changeset 47635 ebb79474262c
parent 47634 091bcd569441
child 47777 f29e7dcd7c40
     1.1 --- a/src/HOL/Library/Quotient_Sum.thy	Fri Apr 20 18:29:21 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Fri Apr 20 22:49:40 2012 +0200
     1.3 @@ -78,7 +78,7 @@
     1.4    "bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (sum_rel R1 R2)"
     1.5    using assms unfolding bi_unique_def split_sum_all by simp
     1.6  
     1.7 -subsection {* Correspondence rules for transfer package *}
     1.8 +subsection {* Transfer rules for transfer package *}
     1.9  
    1.10  lemma Inl_transfer [transfer_rule]: "(A ===> sum_rel A B) Inl Inl"
    1.11    unfolding fun_rel_def by simp