# File Porder.ML

    (* legacy ML bindings *)

    val antisym_less_inverse = thm "antisym_less_inverse";
    val antisym_less = thm "antisym_less";
    val bin_chainmax = thm "bin_chainmax";
    val bin_chain = thm "bin_chain";
    val box_less = thm "box_less";
    val chain_def = thm "chain_def";
    val chainE = thm "chainE";
    val chainI = thm "chainI";
    val chain_const = thm "chain_const";
    val chain_mono3 = thm "chain_mono3";
    val chain_mono = thm "chain_mono";
    val chain_shift = thm "chain_shift";
    val chain_tord = thm "chain_tord";
    val finite_chain_def = thm "finite_chain_def";
    val is_lubD1 = thm "is_lubD1";
    val is_lub_def = thm "is_lub_def";
    val is_lubI = thm "is_lubI";
    val is_lub_lub = thm "is_lub_lub";
    val is_lub_range_shift = thm "is_lub_range_shift";
    val is_ub_def = thm "is_ub_def";
    val is_ub_lub = thm "is_ub_lub";
    val is_ub_range_shift = thm "is_ub_range_shift";
    val lub_bin_chain = thm "lub_bin_chain";
    val lub_chain_maxelem = thm "lub_chain_maxelem";
    val lub_const = thm "lub_const";
    val lub_def = thm "lub_def";
    val lub_finch1 = thm "lub_finch1";
    val lub_finch2 = thm "lub_finch2";
    val lubI = thm "lubI";
    val lub_singleton = thm "lub_singleton";
    val lub = thm "lub";
    val max_in_chain_def = thm "max_in_chain_def";
    val minimal2UU = thm "minimal2UU";
    val po_eq_conv = thm "po_eq_conv";
    val refl_less = thm "refl_less";
    val thelubI = thm "thelubI";
    val tord_def = thm "tord_def";
    val trans_less = thm "trans_less";
    val ub_rangeD = thm "ub_rangeD";
    val ub_rangeI = thm "ub_rangeI";
    val unique_lub = thm "unique_lub";

    structure Porder =
    struct
      val thy = the_context ();
      val is_ub_def = is_ub_def;
      val is_lub_def = is_lub_def;
      val tord_def = tord_def;
      val chain_def = chain_def;
      val max_in_chain_def = max_in_chain_def;
      val finite_chain_def = finite_chain_def;
      val lub_def = lub_def;
    end;