(* legacy ML bindings *)
val order_less_irrefl = thm "order_less_irrefl";
val linorder_not_less = thm "linorder_not_less";
val linorder_not_le = thm "linorder_not_le";
val linorder_neq_iff = thm "linorder_neq_iff";
val linorder_neqE = thm "linorder_neqE";
val order_refl = thm "order_refl";
val order_trans = thm "order_trans";
val order_antisym = thm "order_antisym";
val mono_def = thm "mono_def";
val monoI = thm "monoI";
val monoD = thm "monoD";
val max_less_iff_conj = thm "max_less_iff_conj";
val min_less_iff_conj = thm "min_less_iff_conj";
val split_min = thm "split_min";
val split_max = thm "split_max";