1 |
|
2 (* legacy ML bindings *) |
|
3 |
|
4 val inst_cfun_po = thm "inst_cfun_po"; |
|
5 val less_cfun = thm "less_cfun"; |
|
6 val minimal_cfun = thm "minimal_cfun"; |
|
7 val UU_cfun_def = thm "UU_cfun_def"; |
|
8 val least_cfun = thm "least_cfun"; |
|
9 val cont_Rep_CFun2 = thm "cont_Rep_CFun2"; |
|
10 val monofun_Rep_CFun2 = thm "monofun_Rep_CFun2"; |
|
11 val contlub_Rep_CFun2 = thm "contlub_Rep_CFun2"; |
|
12 val cont_cfun_arg = thm "cont_cfun_arg"; |
|
13 val contlub_cfun_arg = thm "contlub_cfun_arg"; |
|
14 val monofun_Rep_CFun1 = thm "monofun_Rep_CFun1"; |
|
15 val monofun_cfun_fun = thm "monofun_cfun_fun"; |
|
16 val monofun_cfun_arg = thm "monofun_cfun_arg"; |
|
17 val chain_monofun = thm "chain_monofun"; |
|
18 val monofun_cfun = thm "monofun_cfun"; |
|
19 val strictI = thm "strictI"; |
|
20 val ch2ch_Rep_CFunR = thm "ch2ch_Rep_CFunR"; |
|
21 val ch2ch_Rep_CFunL = thm "ch2ch_Rep_CFunL"; |
|
22 val lub_cfun_mono = thm "lub_cfun_mono"; |
|
23 val ex_lubcfun = thm "ex_lubcfun"; |
|
24 val cont_lubcfun = thm "cont_lubcfun"; |
|
25 val lub_cfun = thm "lub_cfun"; |
|
26 val thelub_cfun = thm "thelub_cfun"; |
|
27 val cpo_cfun = thm "cpo_cfun"; |
|
28 val ext_cfun = thm "ext_cfun"; |
|
29 val semi_monofun_Abs_CFun = thm "semi_monofun_Abs_CFun"; |
|
30 val less_cfun2 = thm "less_cfun2"; |
|