| changeset 15576 | efb95d0d01f7 |
| parent 15575 | 63babb1ee883 |
| child 15577 | e16da3068ad6 |
| 15575:63babb1ee883 | 15576:efb95d0d01f7 |
|---|---|
1 |
|
2 (* legacy ML bindings *) |
|
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"; |