src/HOL/Library/Quotient_Sum.thy
changeset 47777 f29e7dcd7c40
parent 47635 ebb79474262c
child 47936 756f30eac792
--- a/src/HOL/Library/Quotient_Sum.thy	Thu Apr 26 01:05:06 2012 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy	Thu Apr 26 12:01:58 2012 +0200
@@ -92,7 +92,7 @@
 
 subsection {* Setup for lifting package *}
 
-lemma Quotient_sum:
+lemma Quotient_sum[quot_map]:
   assumes "Quotient R1 Abs1 Rep1 T1"
   assumes "Quotient R2 Abs2 Rep2 T2"
   shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2)
@@ -100,8 +100,6 @@
   using assms unfolding Quotient_alt_def
   by (simp add: split_sum_all)
 
-declare [[map sum = (sum_rel, Quotient_sum)]]
-
 fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
 where
   "sum_pred R1 R2 (Inl a) = R1 a"