1 |
1 |
2 (* legacy ML bindings *) |
2 (* legacy ML bindings *) |
3 |
3 |
4 val refl_less = thm "refl_less"; |
4 val antisym_less_inverse = thm "antisym_less_inverse"; |
5 val antisym_less = thm "antisym_less"; |
5 val antisym_less = thm "antisym_less"; |
6 val trans_less = thm "trans_less"; |
6 val bin_chainmax = thm "bin_chainmax"; |
7 val minimal2UU = thm "minimal2UU"; |
7 val bin_chain = thm "bin_chain"; |
8 val antisym_less_inverse = thm "antisym_less_inverse"; |
|
9 val box_less = thm "box_less"; |
8 val box_less = thm "box_less"; |
10 val po_eq_conv = thm "po_eq_conv"; |
|
11 val is_ub_def = thm "is_ub_def"; |
|
12 val is_lub_def = thm "is_lub_def"; |
|
13 val tord_def = thm "tord_def"; |
|
14 val chain_def = thm "chain_def"; |
9 val chain_def = thm "chain_def"; |
15 val max_in_chain_def = thm "max_in_chain_def"; |
|
16 val finite_chain_def = thm "finite_chain_def"; |
|
17 val lub_def = thm "lub_def"; |
|
18 val unique_lub = thm "unique_lub"; |
|
19 val chain_mono = thm "chain_mono"; |
|
20 val chain_mono3 = thm "chain_mono3"; |
|
21 val chain_tord = thm "chain_tord"; |
|
22 val lub = thm "lub"; |
|
23 val lubI = thm "lubI"; |
|
24 val thelubI = thm "thelubI"; |
|
25 val lub_singleton = thm "lub_singleton"; |
|
26 val is_lubD1 = thm "is_lubD1"; |
|
27 val is_lub_lub = thm "is_lub_lub"; |
|
28 val is_lubI = thm "is_lubI"; |
|
29 val chainE = thm "chainE"; |
10 val chainE = thm "chainE"; |
30 val chainI = thm "chainI"; |
11 val chainI = thm "chainI"; |
|
12 val chain_mono3 = thm "chain_mono3"; |
|
13 val chain_mono = thm "chain_mono"; |
31 val chain_shift = thm "chain_shift"; |
14 val chain_shift = thm "chain_shift"; |
32 val ub_rangeD = thm "ub_rangeD"; |
15 val chain_tord = thm "chain_tord"; |
33 val ub_rangeI = thm "ub_rangeI"; |
16 val finite_chain_def = thm "finite_chain_def"; |
|
17 val is_lubD1 = thm "is_lubD1"; |
|
18 val is_lub_def = thm "is_lub_def"; |
|
19 val is_lubI = thm "is_lubI"; |
|
20 val is_lub_lub = thm "is_lub_lub"; |
|
21 val is_lub_range_shift = thm "is_lub_range_shift"; |
|
22 val is_ub_def = thm "is_ub_def"; |
34 val is_ub_lub = thm "is_ub_lub"; |
23 val is_ub_lub = thm "is_ub_lub"; |
35 val lub_finch1 = thm "lub_finch1"; |
24 val is_ub_range_shift = thm "is_ub_range_shift"; |
36 val lub_finch2 = thm "lub_finch2"; |
|
37 val bin_chain = thm "bin_chain"; |
|
38 val bin_chainmax = thm "bin_chainmax"; |
|
39 val lub_bin_chain = thm "lub_bin_chain"; |
25 val lub_bin_chain = thm "lub_bin_chain"; |
40 val lub_chain_maxelem = thm "lub_chain_maxelem"; |
26 val lub_chain_maxelem = thm "lub_chain_maxelem"; |
41 val lub_const = thm "lub_const"; |
27 val lub_const = thm "lub_const"; |
|
28 val lub_def = thm "lub_def"; |
|
29 val lub_finch1 = thm "lub_finch1"; |
|
30 val lub_finch2 = thm "lub_finch2"; |
|
31 val lubI = thm "lubI"; |
|
32 val lub_singleton = thm "lub_singleton"; |
|
33 val lub = thm "lub"; |
|
34 val max_in_chain_def = thm "max_in_chain_def"; |
|
35 val minimal2UU = thm "minimal2UU"; |
|
36 val po_eq_conv = thm "po_eq_conv"; |
|
37 val refl_less = thm "refl_less"; |
|
38 val thelubI = thm "thelubI"; |
|
39 val tord_def = thm "tord_def"; |
|
40 val trans_less = thm "trans_less"; |
|
41 val ub_rangeD = thm "ub_rangeD"; |
|
42 val ub_rangeI = thm "ub_rangeI"; |
|
43 val unique_lub = thm "unique_lub"; |
42 |
44 |
43 structure Porder = |
45 structure Porder = |
44 struct |
46 struct |
45 val thy = the_context (); |
47 val thy = the_context (); |
46 val is_ub_def = is_ub_def; |
48 val is_ub_def = is_ub_def; |