changeset 16555 | cec3fbf9832b |
parent 16388 | 1ff571813848 |
child 16630 | 83bf468b1dc7 |
--- a/src/HOLCF/Lift.thy Thu Jun 23 22:08:24 2005 +0200 +++ b/src/HOLCF/Lift.thy Thu Jun 23 22:10:29 2005 +0200 @@ -122,7 +122,7 @@ subsection {* Further operations *} consts - flift1 :: "('a => 'b::pcpo) => ('a lift -> 'b)" + flift1 :: "('a => 'b::pcpo) => ('a lift -> 'b)" (binder "FLIFT " 10) flift2 :: "('a => 'b) => ('a lift -> 'b lift)" liftpair ::"'a::type lift * 'b::type lift => ('a * 'b) lift"