add binder syntax for flift1
authorhuffman
Thu, 23 Jun 2005 22:10:29 +0200
changeset 16555 cec3fbf9832b
parent 16554 5841e7f9eef5
child 16556 a0c8d0499b5f
add binder syntax for flift1
src/HOLCF/Lift.thy
--- 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"