equal
deleted
inserted
replaced
24 Inr :: "'b => 'a+'b" |
24 Inr :: "'b => 'a+'b" |
25 sum_case :: "['a=>'c,'b=>'c, 'a+'b] =>'c" |
25 sum_case :: "['a=>'c,'b=>'c, 'a+'b] =>'c" |
26 |
26 |
27 (*disjoint sum for sets; the operator + is overloaded with wrong type!*) |
27 (*disjoint sum for sets; the operator + is overloaded with wrong type!*) |
28 "plus" :: "['a set, 'b set] => ('a+'b)set" (infixr 65) |
28 "plus" :: "['a set, 'b set] => ('a+'b)set" (infixr 65) |
29 Part :: "['a set, 'a=>'a] => 'a set" |
29 Part :: "['a set, 'b=>'a] => 'a set" |
30 |
30 |
31 translations |
31 translations |
32 "case p of Inl(x) => a | Inr(y) => b" == "sum_case(%x.a, %y.b, p)" |
32 "case p of Inl(x) => a | Inr(y) => b" == "sum_case(%x.a, %y.b, p)" |
33 |
33 |
34 rules |
34 rules |