# File Pcpo.ML

    (* legacy ML bindings *)

    val ax_flat = thm "ax_flat";
    val ch2ch_lub = thm "ch2ch_lub";
    val chain_mono2 = thm "chain_mono2";
    val chain_UU_I_inverse2 = thm "chain_UU_I_inverse2";
    val chain_UU_I_inverse = thm "chain_UU_I_inverse";
    val chain_UU_I = thm "chain_UU_I";
    val chfin2finch = thm "chfin2finch";
    val chfin_imp_cpo = thm "chfin_imp_cpo";
    val chfin = thm "chfin";
    val cpo = thm "cpo";
    val diag_lub = thm "diag_lub";
    val eq_UU_iff = thm "eq_UU_iff";
    val ex_lub = thm "ex_lub";
    val flat_eq = thm "flat_eq";
    val flat_imp_chfin = thm "flat_imp_chfin";
    val increasing_chain_adm_lemma = thm "increasing_chain_adm_lemma";
    val infinite_chain_adm_lemma = thm "infinite_chain_adm_lemma";
    val is_lub_thelub = thm "is_lub_thelub";
    val is_ub_thelub = thm "is_ub_thelub";
    val least = thm "least";
    val lub_equal2 = thm "lub_equal2";
    val lub_equal = thm "lub_equal";
    val lub_mono2 = thm "lub_mono2";
    val lub_mono3 = thm "lub_mono3";
    val lub_mono = thm "lub_mono";
    val lub_range_shift = thm "lub_range_shift";
    val maxinch_is_thelub = thm "maxinch_is_thelub";
    val minimal = thm "minimal";
    val not_less2not_eq = thm "not_less2not_eq";
    val notUU_I = thm "notUU_I";
    val thelubE = thm "thelubE";
    val UU_def = thm "UU_def";
    val UU_I = thm "UU_I";
    val UU_least = thm "UU_least";
    val UU_reorient = thm "UU_reorient";

    structure Pcpo =
    struct
      val thy = the_context ();
      val UU_def = UU_def;
    end;