(* legacy ML bindings *)
val refl_less = thm "refl_less";
val antisym_less = thm "antisym_less";
val trans_less = thm "trans_less";
val minimal2UU = thm "minimal2UU";
val antisym_less_inverse = thm "antisym_less_inverse";
val box_less = thm "box_less";
val po_eq_conv = thm "po_eq_conv";