equal
deleted
inserted
replaced
11 (* new type for strict product *) |
11 (* new type for strict product *) |
12 |
12 |
13 types "**" 2 (infixr 20) |
13 types "**" 2 (infixr 20) |
14 |
14 |
15 arities "**" :: (pcpo,pcpo)term |
15 arities "**" :: (pcpo,pcpo)term |
|
16 |
|
17 syntax (symbols) |
|
18 |
|
19 "**" :: [type, type] => type ("(_ \\<otimes>/ _)" [21,20] 20) |
16 |
20 |
17 consts |
21 consts |
18 Sprod :: "('a => 'b => bool)set" |
22 Sprod :: "('a => 'b => bool)set" |
19 Spair_Rep :: "['a,'b] => ['a,'b] => bool" |
23 Spair_Rep :: "['a,'b] => ['a,'b] => bool" |
20 Rep_Sprod :: "('a ** 'b) => ('a => 'b => bool)" |
24 Rep_Sprod :: "('a ** 'b) => ('a => 'b => bool)" |
48 |
52 |
49 Issnd_def "Issnd(p) == @z. |
53 Issnd_def "Issnd(p) == @z. |
50 (p=Ispair UU UU --> z=UU) |
54 (p=Ispair UU UU --> z=UU) |
51 &(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=b)" |
55 &(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=b)" |
52 |
56 |
53 (* start 8bit 1 *) |
|
54 (* end 8bit 1 *) |
|
55 |
57 |
56 end |
58 end |
57 |
59 |