| changeset 12338 | de0f4a63baa5 |
| parent 12032 | 0f6417c9a187 |
| child 12431 | 07ec657249e5 |
--- a/src/HOLCF/IMP/Denotational.thy Sat Dec 01 18:51:46 2001 +0100 +++ b/src/HOLCF/IMP/Denotational.thy Sat Dec 01 18:52:32 2001 +0100 @@ -9,7 +9,7 @@ Denotational = HOLCF + Natural + constdefs - dlift :: "(('a::term) discr -> 'b::pcpo) => ('a lift -> 'b)" + dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)" "dlift f == (LAM x. case x of UU => UU | Def(y) => f$(Discr y))" consts D :: "com => state discr -> state lift"