1 |
1 |
2 (* legacy ML bindings *) |
2 (* legacy ML bindings *) |
3 |
3 |
|
4 val ax_flat = thm "ax_flat"; |
|
5 val ch2ch_lub = thm "ch2ch_lub"; |
|
6 val chain_mono2 = thm "chain_mono2"; |
|
7 val chain_UU_I_inverse2 = thm "chain_UU_I_inverse2"; |
|
8 val chain_UU_I_inverse = thm "chain_UU_I_inverse"; |
|
9 val chain_UU_I = thm "chain_UU_I"; |
|
10 val chfin2finch = thm "chfin2finch"; |
|
11 val chfin_imp_cpo = thm "chfin_imp_cpo"; |
|
12 val chfin = thm "chfin"; |
4 val cpo = thm "cpo"; |
13 val cpo = thm "cpo"; |
|
14 val diag_lub = thm "diag_lub"; |
|
15 val eq_UU_iff = thm "eq_UU_iff"; |
|
16 val ex_lub = thm "ex_lub"; |
|
17 val flat_eq = thm "flat_eq"; |
|
18 val flat_imp_chfin = thm "flat_imp_chfin"; |
|
19 val increasing_chain_adm_lemma = thm "increasing_chain_adm_lemma"; |
|
20 val infinite_chain_adm_lemma = thm "infinite_chain_adm_lemma"; |
|
21 val is_lub_thelub = thm "is_lub_thelub"; |
|
22 val is_ub_thelub = thm "is_ub_thelub"; |
5 val least = thm "least"; |
23 val least = thm "least"; |
6 val UU_def = thm "UU_def"; |
24 val lub_equal2 = thm "lub_equal2"; |
7 val chfin = thm "chfin"; |
25 val lub_equal = thm "lub_equal"; |
8 val ax_flat = thm "ax_flat"; |
26 val lub_mono2 = thm "lub_mono2"; |
9 val UU_least = thm "UU_least"; |
27 val lub_mono3 = thm "lub_mono3"; |
10 val minimal = thm "minimal"; |
28 val lub_mono = thm "lub_mono"; |
11 val thelubE = thm "thelubE"; |
|
12 val is_ub_thelub = thm "is_ub_thelub"; |
|
13 val is_lub_thelub = thm "is_lub_thelub"; |
|
14 val lub_range_shift = thm "lub_range_shift"; |
29 val lub_range_shift = thm "lub_range_shift"; |
15 val maxinch_is_thelub = thm "maxinch_is_thelub"; |
30 val maxinch_is_thelub = thm "maxinch_is_thelub"; |
16 val lub_mono = thm "lub_mono"; |
31 val minimal = thm "minimal"; |
17 val lub_equal = thm "lub_equal"; |
32 val not_less2not_eq = thm "not_less2not_eq"; |
18 val lub_mono2 = thm "lub_mono2"; |
33 val notUU_I = thm "notUU_I"; |
19 val lub_equal2 = thm "lub_equal2"; |
34 val thelubE = thm "thelubE"; |
20 val lub_mono3 = thm "lub_mono3"; |
35 val UU_def = thm "UU_def"; |
21 val eq_UU_iff = thm "eq_UU_iff"; |
|
22 val UU_I = thm "UU_I"; |
36 val UU_I = thm "UU_I"; |
23 val not_less2not_eq = thm "not_less2not_eq"; |
37 val UU_least = thm "UU_least"; |
24 val chain_UU_I = thm "chain_UU_I"; |
38 val UU_reorient = thm "UU_reorient"; |
25 val chain_UU_I_inverse = thm "chain_UU_I_inverse"; |
|
26 val chain_UU_I_inverse2 = thm "chain_UU_I_inverse2"; |
|
27 val notUU_I = thm "notUU_I"; |
|
28 val chain_mono2 = thm "chain_mono2"; |
|
29 val flat_imp_chfin = thm "flat_imp_chfin"; |
|
30 val flat_eq = thm "flat_eq"; |
|
31 val chfin2finch = thm "chfin2finch"; |
|
32 val infinite_chain_adm_lemma = thm "infinite_chain_adm_lemma"; |
|
33 val increasing_chain_adm_lemma = thm "increasing_chain_adm_lemma"; |
|
34 |
39 |
35 structure Pcpo = |
40 structure Pcpo = |
36 struct |
41 struct |
37 val thy = the_context (); |
42 val thy = the_context (); |
38 val UU_def = UU_def; |
43 val UU_def = UU_def; |