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