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