(* legacy ML bindings *)
val less_cprod_def = thm "less_cprod_def";
val refl_less_cprod = thm "refl_less_cprod";
val antisym_less_cprod = thm "antisym_less_cprod";
val trans_less_cprod = thm "trans_less_cprod";
val minimal_cprod = thm "minimal_cprod";
val least_cprod = thm "least_cprod";
val monofun_pair1 = thm "monofun_pair1";
val monofun_pair2 = thm "monofun_pair2";
val monofun_pair = thm "monofun_pair";
val monofun_fst = thm "monofun_fst";
val monofun_snd = thm "monofun_snd";
val lub_cprod = thm "lub_cprod";
val thelub_cprod = thm "thelub_cprod";
val cpo_cprod = thm "cpo_cprod";
val cpair_def = thm "cpair_def";
val cfst_def = thm "cfst_def";
val csnd_def = thm "csnd_def";
val csplit_def = thm "csplit_def";
val CLet_def = thm "CLet_def";
val inst_cprod_pcpo = thm "inst_cprod_pcpo";
val contlub_pair1 = thm "contlub_pair1";
val contlub_pair2 = thm "contlub_pair2";
val cont_pair1 = thm "cont_pair1";
val cont_pair2 = thm "cont_pair2";
val contlub_fst = thm "contlub_fst";
val contlub_snd = thm "contlub_snd";
val cont_fst = thm "cont_fst";
val cont_snd = thm "cont_snd";
val inject_cpair = thm "inject_cpair";
val inst_cprod_pcpo2 = thm "inst_cprod_pcpo2";
val defined_cpair_rev = thm "defined_cpair_rev";
val Exh_Cprod2 = thm "Exh_Cprod2";
val cprodE = thm "cprodE";
val cfst_cpair = thm "cfst_cpair";
val csnd_cpair = thm "csnd_cpair";
val cfst_strict = thm "cfst_strict";
val csnd_strict = thm "csnd_strict";
val surjective_pairing_Cprod2 = thm "surjective_pairing_Cprod2";
val lub_cprod2 = thm "lub_cprod2";
val thelub_cprod2 = thm "thelub_cprod2";
val csplit2 = thm "csplit2";
val csplit3 = thm "csplit3";
val Cprod_rews = [cfst_cpair, csnd_cpair, csplit2];