src/HOL/Library/Quotient_Sum.thy
changeset 45802 b16f976db515
parent 41372 551eb49a6e91
child 47094 1a7ad2601cb5
     1.1 --- a/src/HOL/Library/Quotient_Sum.thy	Fri Dec 09 16:08:32 2011 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Fri Dec 09 18:07:04 2011 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  | "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
     1.5  | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
     1.6  
     1.7 -declare [[map sum = (sum_map, sum_rel)]]
     1.8 +declare [[map sum = sum_rel]]
     1.9  
    1.10  lemma sum_rel_unfold:
    1.11    "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y