| changeset 2838 | 2e908f29bc3d |
| parent 2640 | ee4dfce170a0 |
| child 3327 | 9b8e638f8602 |
| 2837:dee1c7f1f576 | 2838:2e908f29bc3d |
|---|---|
7 |
7 |
8 *) |
8 *) |
9 |
9 |
10 Cfun3 = Cfun2 + |
10 Cfun3 = Cfun2 + |
11 |
11 |
12 instance "->" :: (pcpo,pcpo)pcpo (least_cfun,cpo_cfun) |
12 instance "->" :: (cpo,cpo)cpo (cpo_cfun) |
13 instance "->" :: (cpo,pcpo)pcpo (least_cfun) |
|
14 |
|
15 default pcpo |
|
13 |
16 |
14 consts |
17 consts |
15 Istrictify :: "('a->'b)=>'a=>'b" |
18 Istrictify :: "('a->'b)=>'a=>'b" |
16 strictify :: "('a->'b)->'a->'b" |
19 strictify :: "('a->'b)->'a->'b" |
17 defs |
20 defs |