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