src/HOL/Library/Quotient_Sum.thy
changeset 40542 9a173a22771c
parent 40465 2989f9f3aa10
child 40610 70776ecfe324
     1.1 --- a/src/HOL/Library/Quotient_Sum.thy	Mon Nov 15 14:14:38 2010 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Mon Nov 15 14:59:21 2010 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  begin
     1.5  
     1.6  fun
     1.7 -  sum_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
     1.8 +  sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
     1.9  where
    1.10    "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
    1.11  | "sum_rel R1 R2 (Inl a1) (Inr b2) = False"