1 |
1 |
2 (* legacy ML bindings *) |
2 (* legacy ML bindings *) |
3 |
3 |
|
4 val binchain_cont = thm "binchain_cont"; |
|
5 val ch2ch_cont = thm "ch2ch_cont"; |
|
6 val ch2ch_monofun = thm "ch2ch_monofun"; |
|
7 val chfindom_monofun2cont = thm "chfindom_monofun2cont"; |
|
8 val cont2cont_app2 = thm "cont2cont_app2"; |
|
9 val cont2cont_app3 = thm "cont2cont_app3"; |
|
10 val cont2cont_app = thm "cont2cont_app"; |
|
11 val cont2cont_CF1L_rev = thm "cont2cont_CF1L_rev"; |
|
12 val cont2cont_CF1L = thm "cont2cont_CF1L"; |
|
13 val cont2cont_lambda = thm "cont2cont_lambda"; |
|
14 val cont2contlub_app = thm "cont2contlub_app"; |
|
15 val cont2contlubE = thm "cont2contlubE"; |
|
16 val cont2cont_lub = thm "cont2cont_lub"; |
|
17 val cont2contlub = thm "cont2contlub"; |
|
18 val cont2mono = thm "cont2mono"; |
|
19 val cont_const = thm "cont_const"; |
|
20 val cont_def = thm "cont_def"; |
|
21 val contE = thm "contE"; |
|
22 val cont_finch2finch = thm "cont_finch2finch"; |
|
23 val cont_id = thm "cont_id"; |
|
24 val cont_if = thm "cont_if"; |
|
25 val contI = thm "contI"; |
|
26 val contlub_abstraction = thm "contlub_abstraction"; |
|
27 val contlub_def = thm "contlub_def"; |
|
28 val contlubE = thm "contlubE"; |
|
29 val contlubI = thm "contlubI"; |
|
30 val contlub_lub_fun = thm "contlub_lub_fun"; |
|
31 val flatdom_strict2cont = thm "flatdom_strict2cont"; |
|
32 val flatdom_strict2mono = thm "flatdom_strict2mono"; |
|
33 val mono2mono_app = thm "mono2mono_app"; |
|
34 val mono2mono_MF1L_rev = thm "mono2mono_MF1L_rev"; |
|
35 val mono2mono_MF1L = thm "mono2mono_MF1L"; |
|
36 val monocontlub2cont = thm "monocontlub2cont"; |
4 val monofun_def = thm "monofun_def"; |
37 val monofun_def = thm "monofun_def"; |
5 val contlub_def = thm "contlub_def"; |
38 val monofunE = thm "monofunE"; |
6 val cont_def = thm "cont_def"; |
39 val monofun_finch2finch = thm "monofun_finch2finch"; |
7 val contlubI = thm "contlubI"; |
40 val monofun_fun_arg = thm "monofun_fun_arg"; |
8 val contlubE = thm "contlubE"; |
41 val monofun_fun_fun = thm "monofun_fun_fun"; |
9 val contI = thm "contI"; |
42 val monofun_fun = thm "monofun_fun"; |
10 val contE = thm "contE"; |
|
11 val monofunI = thm "monofunI"; |
43 val monofunI = thm "monofunI"; |
12 val monofunE = thm "monofunE"; |
44 val monofun_lub_fun = thm "monofun_lub_fun"; |
13 val ch2ch_monofun = thm "ch2ch_monofun"; |
|
14 val ub2ub_monofun = thm "ub2ub_monofun"; |
45 val ub2ub_monofun = thm "ub2ub_monofun"; |
15 val monocontlub2cont = thm "monocontlub2cont"; |
|
16 val binchain_cont = thm "binchain_cont"; |
|
17 val cont2mono = thm "cont2mono"; |
|
18 val cont2contlub = thm "cont2contlub"; |
|
19 val monofun_finch2finch = thm "monofun_finch2finch"; |
|
20 val cont_finch2finch = thm "cont_finch2finch"; |
|
21 val monofun_fun_fun = thm "monofun_fun_fun"; |
|
22 val monofun_fun_arg = thm "monofun_fun_arg"; |
|
23 val mono2mono_MF1L = thm "mono2mono_MF1L"; |
|
24 val cont2cont_CF1L = thm "cont2cont_CF1L"; |
|
25 val mono2mono_MF1L_rev = thm "mono2mono_MF1L_rev"; |
|
26 val cont2cont_CF1L_rev = thm "cont2cont_CF1L_rev"; |
|
27 val cont2cont_lambda = thm "cont2cont_lambda"; |
|
28 val contlub_abstraction = thm "contlub_abstraction"; |
|
29 val mono2mono_app = thm "mono2mono_app"; |
|
30 val cont2contlub_app = thm "cont2contlub_app"; |
|
31 val cont2cont_app = thm "cont2cont_app"; |
|
32 val cont2cont_app2 = thm "cont2cont_app2"; |
|
33 val cont_id = thm "cont_id"; |
|
34 val cont_const = thm "cont_const"; |
|
35 val cont2cont_app3 = thm "cont2cont_app3"; |
|
36 val chfindom_monofun2cont = thm "chfindom_monofun2cont"; |
|
37 val flatdom_strict2mono = thm "flatdom_strict2mono"; |
|
38 val flatdom_strict2cont = thm "flatdom_strict2cont"; |
|