equal
deleted
inserted
replaced
17 typedef (Ssum) ('a, 'b) "++" (infixr 10) = |
17 typedef (Ssum) ('a, 'b) "++" (infixr 10) = |
18 "{f.(? a. f=Sinl_Rep(a::'a))|(? b. f=Sinr_Rep(b::'b))}" |
18 "{f.(? a. f=Sinl_Rep(a::'a))|(? b. f=Sinr_Rep(b::'b))}" |
19 |
19 |
20 syntax (xsymbols) |
20 syntax (xsymbols) |
21 "++" :: [type, type] => type ("(_ \\<oplus>/ _)" [21, 20] 20) |
21 "++" :: [type, type] => type ("(_ \\<oplus>/ _)" [21, 20] 20) |
|
22 syntax (HTML output) |
|
23 "++" :: [type, type] => type ("(_ \\<oplus>/ _)" [21, 20] 20) |
22 |
24 |
23 consts |
25 consts |
24 Isinl :: "'a => ('a ++ 'b)" |
26 Isinl :: "'a => ('a ++ 'b)" |
25 Isinr :: "'b => ('a ++ 'b)" |
27 Isinr :: "'b => ('a ++ 'b)" |
26 Iwhen :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c" |
28 Iwhen :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c" |