equal
deleted
inserted
replaced
16 |
16 |
17 defs |
17 defs |
18 Inl_Rep_def "Inl_Rep == (%a. %x y p. x=a & p)" |
18 Inl_Rep_def "Inl_Rep == (%a. %x y p. x=a & p)" |
19 Inr_Rep_def "Inr_Rep == (%b. %x y p. y=b & ~p)" |
19 Inr_Rep_def "Inr_Rep == (%b. %x y p. y=b & ~p)" |
20 |
20 |
21 subtype (Sum) |
21 typedef (Sum) |
22 ('a, 'b) "+" (infixr 10) |
22 ('a, 'b) "+" (infixr 10) |
23 = "{f. (? a. f = Inl_Rep(a::'a)) | (? b. f = Inr_Rep(b::'b))}" |
23 = "{f. (? a. f = Inl_Rep(a::'a)) | (? b. f = Inr_Rep(b::'b))}" |
24 |
24 |
25 |
25 |
26 (* abstract constants and syntax *) |
26 (* abstract constants and syntax *) |