| changeset 22838 | 466599ecf610 |
| parent 22622 | 25693088396b |
| child 25534 | d0b74fdd6067 |
| 22837:82cceaf768c8 | 22838:466599ecf610 |
|---|---|
21 |
21 |
22 |
22 |
23 global |
23 global |
24 |
24 |
25 typedef (Sum) |
25 typedef (Sum) |
26 ('a, 'b) "+" (infixr 10) |
26 ('a, 'b) "+" (infixr "+" 10) |
27 = "{f. (? a. f = Inl_Rep(a::'a)) | (? b. f = Inr_Rep(b::'b))}" |
27 = "{f. (? a. f = Inl_Rep(a::'a)) | (? b. f = Inr_Rep(b::'b))}" |
28 by auto |
28 by auto |
29 |
29 |
30 local |
30 local |
31 |
31 |