src/HOLCF/Cfun1.thy
changeset 10863 fef84fefd33f
parent 10834 a7897aebbffc
child 12030 46d57d0290a2
     1.1 --- a/src/HOLCF/Cfun1.thy	Wed Jan 10 20:21:11 2001 +0100
     1.2 +++ b/src/HOLCF/Cfun1.thy	Wed Jan 10 20:41:14 2001 +0100
     1.3 @@ -17,9 +17,9 @@
     1.4  instance "->"  :: (cpo,cpo)sq_ord
     1.5  
     1.6  syntax
     1.7 -	Rep_CFun  :: "('a -> 'b)=>('a => 'b)" ("_$_" [999,1000] 999)
     1.8 +	Rep_CFun  :: "('a -> 'b) => ('a => 'b)" ("_$_" [999,1000] 999)
     1.9                                                  (* application      *)
    1.10 -        Abs_CFun  :: "('a => 'b)=>('a -> 'b)"     (binder "LAM " 10)
    1.11 +        Abs_CFun  :: "('a => 'b) => ('a -> 'b)" (binder "LAM " 10)
    1.12                                                  (* abstraction      *)
    1.13          less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
    1.14  
    1.15 @@ -27,6 +27,11 @@
    1.16    "->"		:: [type, type] => type	("(_ \\<rightarrow>/ _)" [1,0]0)
    1.17    "LAM "	:: "[idts, 'a => 'b] => ('a -> 'b)"
    1.18  					("(3\\<Lambda>_./ _)" [0, 10] 10)
    1.19 +  Rep_CFun      :: "('a -> 'b) => ('a => 'b)"  ("(_\\<cdot>_)" [999,1000] 999)
    1.20 +
    1.21 +syntax (HTML output)
    1.22 +  Rep_CFun      :: "('a -> 'b) => ('a => 'b)"  ("(_\\<cdot>_)" [999,1000] 999)
    1.23 +
    1.24  defs 
    1.25    less_cfun_def "(op <<) == (% fo1 fo2. Rep_CFun fo1 << Rep_CFun fo2 )"
    1.26