equal
deleted
inserted
replaced
8 |
8 |
9 Denotational = HOLCF + Natural + |
9 Denotational = HOLCF + Natural + |
10 |
10 |
11 constdefs |
11 constdefs |
12 dlift :: "(('a::term) discr -> 'b::pcpo) => ('a lift -> 'b)" |
12 dlift :: "(('a::term) discr -> 'b::pcpo) => ('a lift -> 'b)" |
13 "dlift f == (LAM x. case x of Undef => UU | Def(y) => f$(Discr y))" |
13 "dlift f == (LAM x. case x of UU => UU | Def(y) => f$(Discr y))" |
14 |
14 |
15 consts D :: "com => state discr -> state lift" |
15 consts D :: "com => state discr -> state lift" |
16 |
16 |
17 primrec |
17 primrec |
18 "D(SKIP) = (LAM s. Def(undiscr s))" |
18 "D(SKIP) = (LAM s. Def(undiscr s))" |