equal
deleted
inserted
replaced
1 |
1 |
2 (* legacy ML bindings *) |
2 (* legacy ML bindings *) |
3 |
3 |
|
4 val refl_less = thm "refl_less"; |
|
5 val antisym_less = thm "antisym_less"; |
|
6 val trans_less = thm "trans_less"; |
|
7 val minimal2UU = thm "minimal2UU"; |
|
8 val antisym_less_inverse = thm "antisym_less_inverse"; |
|
9 val box_less = thm "box_less"; |
|
10 val po_eq_conv = thm "po_eq_conv"; |
4 val is_ub_def = thm "is_ub_def"; |
11 val is_ub_def = thm "is_ub_def"; |
5 val is_lub_def = thm "is_lub_def"; |
12 val is_lub_def = thm "is_lub_def"; |
6 val tord_def = thm "tord_def"; |
13 val tord_def = thm "tord_def"; |
7 val chain_def = thm "chain_def"; |
14 val chain_def = thm "chain_def"; |
8 val max_in_chain_def = thm "max_in_chain_def"; |
15 val max_in_chain_def = thm "max_in_chain_def"; |