src/HOLCF/Cfun1.thy
changeset 10834 a7897aebbffc
parent 6382 8b0c9205da75
child 10863 fef84fefd33f
equal deleted inserted replaced
10833:c0844a30ea4e 10834:a7897aebbffc
    15 
    15 
    16 (* to make << defineable *)
    16 (* to make << defineable *)
    17 instance "->"  :: (cpo,cpo)sq_ord
    17 instance "->"  :: (cpo,cpo)sq_ord
    18 
    18 
    19 syntax
    19 syntax
    20 	Rep_CFun  :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999)
    20 	Rep_CFun  :: "('a -> 'b)=>('a => 'b)" ("_$_" [999,1000] 999)
    21                                                 (* application      *)
    21                                                 (* application      *)
    22         Abs_CFun  :: "('a => 'b)=>('a -> 'b)"     (binder "LAM " 10)
    22         Abs_CFun  :: "('a => 'b)=>('a -> 'b)"     (binder "LAM " 10)
    23                                                 (* abstraction      *)
    23                                                 (* abstraction      *)
    24         less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
    24         less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
    25 
    25