equal
deleted
inserted
replaced
13 "Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a & y=b ))" |
13 "Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a & y=b ))" |
14 |
14 |
15 typedef (Sprod) ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep (a::'a) (b::'b)}" |
15 typedef (Sprod) ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep (a::'a) (b::'b)}" |
16 |
16 |
17 syntax (xsymbols) |
17 syntax (xsymbols) |
|
18 "**" :: [type, type] => type ("(_ \\<otimes>/ _)" [21,20] 20) |
|
19 syntax (HTML output) |
18 "**" :: [type, type] => type ("(_ \\<otimes>/ _)" [21,20] 20) |
20 "**" :: [type, type] => type ("(_ \\<otimes>/ _)" [21,20] 20) |
19 |
21 |
20 consts |
22 consts |
21 Ispair :: "['a,'b] => ('a ** 'b)" |
23 Ispair :: "['a,'b] => ('a ** 'b)" |
22 Isfst :: "('a ** 'b) => 'a" |
24 Isfst :: "('a ** 'b) => 'a" |