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 |
26 syntax (symbols) |
26 syntax (symbols) |
27 "->" :: [type, type] => type ("(_ \\<rightarrow>/ _)" [1,0]0) |
27 "->" :: [type, type] => type ("(_ \\<rightarrow>/ _)" [1,0]0) |
28 "LAM " :: "[idts, 'a => 'b] => ('a -> 'b)" |
28 "LAM " :: "[idts, 'a => 'b] => ('a -> 'b)" |
29 ("(3\\<Lambda>_./ _)" [0, 10] 10) |
29 ("(3\\<Lambda>_./ _)" [0, 10] 10) |
|
30 Rep_CFun :: "('a -> 'b) => ('a => 'b)" ("(_\\<cdot>_)" [999,1000] 999) |
|
31 |
|
32 syntax (HTML output) |
|
33 Rep_CFun :: "('a -> 'b) => ('a => 'b)" ("(_\\<cdot>_)" [999,1000] 999) |
|
34 |
30 defs |
35 defs |
31 less_cfun_def "(op <<) == (% fo1 fo2. Rep_CFun fo1 << Rep_CFun fo2 )" |
36 less_cfun_def "(op <<) == (% fo1 fo2. Rep_CFun fo1 << Rep_CFun fo2 )" |
32 |
37 |
33 end |
38 end |