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