src/HOL/Library/Quotient_Sum.thy
changeset 40610 70776ecfe324
parent 40542 9a173a22771c
child 40820 fd9c98ead9a9
     1.1 --- a/src/HOL/Library/Quotient_Sum.thy	Thu Nov 18 17:01:16 2010 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Thu Nov 18 17:01:16 2010 +0100
     1.3 @@ -16,12 +16,6 @@
     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 -primrec
     1.8 -  sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd"
     1.9 -where
    1.10 -  "sum_map f1 f2 (Inl a) = Inl (f1 a)"
    1.11 -| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
    1.12 -
    1.13  declare [[map sum = (sum_map, sum_rel)]]
    1.14  
    1.15