|
1 |
|
2 (* legacy ML bindings *) |
|
3 |
|
4 val Iup_def = thm "Iup_def"; |
|
5 val Ifup_def = thm "Ifup_def"; |
|
6 val less_up_def = thm "less_up_def"; |
|
7 val Abs_Up_inverse2 = thm "Abs_Up_inverse2"; |
|
8 val Exh_Up = thm "Exh_Up"; |
|
9 val inj_Abs_Up = thm "inj_Abs_Up"; |
|
10 val inj_Rep_Up = thm "inj_Rep_Up"; |
|
11 val inject_Iup = thm "inject_Iup"; |
|
12 val defined_Iup = thm "defined_Iup"; |
|
13 val upE = thm "upE"; |
|
14 val Ifup1 = thm "Ifup1"; |
|
15 val Ifup2 = thm "Ifup2"; |
|
16 val less_up1a = thm "less_up1a"; |
|
17 val less_up1b = thm "less_up1b"; |
|
18 val less_up1c = thm "less_up1c"; |
|
19 val refl_less_up = thm "refl_less_up"; |
|
20 val antisym_less_up = thm "antisym_less_up"; |
|
21 val trans_less_up = thm "trans_less_up"; |
|
22 val inst_up_po = thm "inst_up_po"; |
|
23 val minimal_up = thm "minimal_up"; |
|
24 val UU_up_def = thm "UU_up_def"; |
|
25 val least_up = thm "least_up"; |
|
26 val less_up2b = thm "less_up2b"; |
|
27 val less_up2c = thm "less_up2c"; |
|
28 val monofun_Iup = thm "monofun_Iup"; |
|
29 val monofun_Ifup1 = thm "monofun_Ifup1"; |
|
30 val monofun_Ifup2 = thm "monofun_Ifup2"; |
|
31 val up_lemma1 = thm "up_lemma1"; |
|
32 val lub_up1a = thm "lub_up1a"; |
|
33 val lub_up1b = thm "lub_up1b"; |
|
34 val thelub_up1a = thm "thelub_up1a"; |
|
35 val thelub_up1b = thm "thelub_up1b"; |
|
36 val cpo_up = thm "cpo_up"; |
|
37 val up_def = thm "up_def"; |
|
38 val fup_def = thm "fup_def"; |
|
39 val inst_up_pcpo = thm "inst_up_pcpo"; |
|
40 val less_up3b = thm "less_up3b"; |
|
41 val defined_Iup2 = thm "defined_Iup2"; |
|
42 val contlub_Iup = thm "contlub_Iup"; |
|
43 val cont_Iup = thm "cont_Iup"; |
|
44 val contlub_Ifup1 = thm "contlub_Ifup1"; |
|
45 val contlub_Ifup2 = thm "contlub_Ifup2"; |
|
46 val cont_Ifup1 = thm "cont_Ifup1"; |
|
47 val cont_Ifup2 = thm "cont_Ifup2"; |
|
48 val Exh_Up1 = thm "Exh_Up1"; |
|
49 val inject_up = thm "inject_up"; |
|
50 val defined_up = thm "defined_up"; |
|
51 val upE1 = thm "upE1"; |
|
52 val fup1 = thm "fup1"; |
|
53 val fup2 = thm "fup2"; |
|
54 val less_up4b = thm "less_up4b"; |
|
55 val less_up4c = thm "less_up4c"; |
|
56 val thelub_up2a = thm "thelub_up2a"; |
|
57 val thelub_up2b = thm "thelub_up2b"; |
|
58 val up_lemma2 = thm "up_lemma2"; |
|
59 val thelub_up2a_rev = thm "thelub_up2a_rev"; |
|
60 val thelub_up2b_rev = thm "thelub_up2b_rev"; |
|
61 val thelub_up3 = thm "thelub_up3"; |
|
62 val fup3 = thm "fup3"; |