# HG changeset patch
# User huffman
# Date 1119557429 -7200
# Node ID cec3fbf9832bbffd9b959582fe2b0857f685d449
# Parent  5841e7f9eef5ee1eabd21679d72358b1807ad68f
add binder syntax for flift1

diff -r 5841e7f9eef5 -r cec3fbf9832b 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"