src/HOL/Library/Quotient_Sum.thy
changeset 37678 0040bafffdef
parent 35788 f1deaca15ca3
child 39198 f967a16dfcdd
     1.1 --- a/src/HOL/Library/Quotient_Sum.thy	Thu Jul 01 16:54:42 2010 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Thu Jul 01 16:54:44 2010 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4    "sum_map f1 f2 (Inl a) = Inl (f1 a)"
     1.5  | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
     1.6  
     1.7 -declare [[map "+" = (sum_map, sum_rel)]]
     1.8 +declare [[map sum = (sum_map, sum_rel)]]
     1.9  
    1.10  
    1.11  text {* should probably be in @{theory Sum_Type} *}