1 (* legacy ML bindings *) |
1 (* legacy ML bindings *) |
2 |
2 |
3 val Least_def = thm "Least_def"; |
|
4 val Least_equality = thm "Least_equality"; |
|
5 val mono_def = thm "mono_def"; |
|
6 val monoI = thm "monoI"; |
|
7 val monoD = thm "monoD"; |
|
8 val min_def = thm "min_def"; |
|
9 val min_of_mono = thm "min_of_mono"; |
|
10 val max_def = thm "max_def"; |
|
11 val max_of_mono = thm "max_of_mono"; |
|
12 val min_leastL = thm "min_leastL"; |
|
13 val max_leastL = thm "max_leastL"; |
|
14 val min_leastR = thm "min_leastR"; |
|
15 val max_leastR = thm "max_leastR"; |
|
16 val order_eq_refl = thm "order_eq_refl"; |
3 val order_eq_refl = thm "order_eq_refl"; |
17 val order_less_irrefl = thm "order_less_irrefl"; |
4 val order_less_irrefl = thm "order_less_irrefl"; |
18 val order_le_less = thm "order_le_less"; |
5 val order_le_less = thm "order_le_less"; |
19 val order_le_imp_less_or_eq = thm "order_le_imp_less_or_eq"; |
6 val order_le_imp_less_or_eq = thm "order_le_imp_less_or_eq"; |
20 val order_less_imp_le = thm "order_less_imp_le"; |
7 val order_less_imp_le = thm "order_less_imp_le"; |
31 val linorder_cases = thm "linorder_cases"; |
18 val linorder_cases = thm "linorder_cases"; |
32 val linorder_not_less = thm "linorder_not_less"; |
19 val linorder_not_less = thm "linorder_not_less"; |
33 val linorder_not_le = thm "linorder_not_le"; |
20 val linorder_not_le = thm "linorder_not_le"; |
34 val linorder_neq_iff = thm "linorder_neq_iff"; |
21 val linorder_neq_iff = thm "linorder_neq_iff"; |
35 val linorder_neqE = thm "linorder_neqE"; |
22 val linorder_neqE = thm "linorder_neqE"; |
36 (* |
|
37 val min_same = thm "min_same"; |
|
38 val max_same = thm "max_same"; |
|
39 *) |
|
40 val le_max_iff_disj = thm "le_max_iff_disj"; |
|
41 val le_maxI1 = thm "le_maxI1"; |
|
42 val le_maxI2 = thm "le_maxI2"; |
|
43 val less_max_iff_disj = thm "less_max_iff_disj"; |
|
44 val max_less_iff_conj = thm "max_less_iff_conj"; |
|
45 val min_less_iff_conj = thm "min_less_iff_conj"; |
|
46 val min_le_iff_disj = thm "min_le_iff_disj"; |
|
47 val min_less_iff_disj = thm "min_less_iff_disj"; |
|
48 val split_min = thm "split_min"; |
|
49 val split_max = thm "split_max"; |
|
50 val order_refl = thm "order_refl"; |
23 val order_refl = thm "order_refl"; |
51 val order_trans = thm "order_trans"; |
24 val order_trans = thm "order_trans"; |
52 val order_antisym = thm "order_antisym"; |
25 val order_antisym = thm "order_antisym"; |
53 val order_less_le = thm "order_less_le"; |
26 val order_less_le = thm "order_less_le"; |
54 val linorder_linear = thm "linorder_linear"; |
27 val linorder_linear = thm "linorder_linear"; |
|
28 val mono_def = thm "mono_def"; |
|
29 val monoI = thm "monoI"; |
|
30 val monoD = thm "monoD"; |