changeset 122 | 6927e1cb2c07 |
parent 117 | 3716c99fb6a1 |
child 128 | 89669c58e506 |
--- a/Sum.thy Fri Aug 19 16:18:44 1994 +0200 +++ b/Sum.thy Mon Aug 22 10:56:45 1994 +0200 @@ -26,7 +26,7 @@ (*disjoint sum for sets; the operator + is overloaded with wrong type!*) "plus" :: "['a set, 'b set] => ('a+'b)set" (infixr 65) - Part :: "['a set, 'a=>'a] => 'a set" + Part :: "['a set, 'b=>'a] => 'a set" translations "case p of Inl(x) => a | Inr(y) => b" == "sum_case(%x.a, %y.b, p)"