equal
deleted
inserted
replaced
1 |
1 |
2 (* legacy ML bindings *) |
2 (* legacy ML bindings *) |
3 |
3 |
4 val Iup_def = thm "Iup_def"; |
|
5 val Ifup_def = thm "Ifup_def"; |
|
6 val less_up_def = thm "less_up_def"; |
4 val less_up_def = thm "less_up_def"; |
7 val Ifup1 = thm "Ifup1"; |
|
8 val Ifup2 = thm "Ifup2"; |
|
9 val refl_less_up = thm "refl_less_up"; |
5 val refl_less_up = thm "refl_less_up"; |
10 val antisym_less_up = thm "antisym_less_up"; |
6 val antisym_less_up = thm "antisym_less_up"; |
11 val trans_less_up = thm "trans_less_up"; |
7 val trans_less_up = thm "trans_less_up"; |
12 val minimal_up = thm "minimal_up"; |
8 val minimal_up = thm "minimal_up"; |
13 val least_up = thm "least_up"; |
9 val least_up = thm "least_up"; |
18 val fup_def = thm "fup_def"; |
14 val fup_def = thm "fup_def"; |
19 val inst_up_pcpo = thm "inst_up_pcpo"; |
15 val inst_up_pcpo = thm "inst_up_pcpo"; |
20 val cont_Iup = thm "cont_Iup"; |
16 val cont_Iup = thm "cont_Iup"; |
21 val cont_Ifup1 = thm "cont_Ifup1"; |
17 val cont_Ifup1 = thm "cont_Ifup1"; |
22 val cont_Ifup2 = thm "cont_Ifup2"; |
18 val cont_Ifup2 = thm "cont_Ifup2"; |
23 val Exh_Up1 = thm "Exh_Up1"; |
19 val Exh_Up = thm "Exh_Up"; |
24 val up_inject = thm "up_inject"; |
20 val up_inject = thm "up_inject"; |
25 val up_eq = thm "up_eq"; |
21 val up_eq = thm "up_eq"; |
26 val up_defined = thm "up_defined"; |
22 val up_defined = thm "up_defined"; |
27 val up_less = thm "up_less"; |
23 val up_less = thm "up_less"; |
28 val upE1 = thm "upE1"; |
24 val upE = thm "upE"; |
29 val fup1 = thm "fup1"; |
25 val fup1 = thm "fup1"; |
30 val fup2 = thm "fup2"; |
26 val fup2 = thm "fup2"; |
31 val fup3 = thm "fup3"; |
27 val fup3 = thm "fup3"; |