equal
deleted
inserted
replaced
11 imports "../BNF" |
11 imports "../BNF" |
12 begin |
12 begin |
13 |
13 |
14 hide_fact (open) Quotient_Product.prod_rel_def |
14 hide_fact (open) Quotient_Product.prod_rel_def |
15 |
15 |
16 codata 'a process = |
16 codatatype 'a process = |
17 isAction: Action (prefOf: 'a) (contOf: "'a process") | |
17 isAction: Action (prefOf: 'a) (contOf: "'a process") | |
18 isChoice: Choice (ch1Of: "'a process") (ch2Of: "'a process") |
18 isChoice: Choice (ch1Of: "'a process") (ch2Of: "'a process") |
19 |
19 |
20 (* Read: prefix of, continuation of, choice 1 of, choice 2 of *) |
20 (* Read: prefix of, continuation of, choice 1 of, choice 2 of *) |
21 |
21 |