--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Up.ML Fri Mar 04 23:12:36 2005 +0100
@@ -0,0 +1,62 @@
+
+(* legacy ML bindings *)
+
+val Iup_def = thm "Iup_def";
+val Ifup_def = thm "Ifup_def";
+val less_up_def = thm "less_up_def";
+val Abs_Up_inverse2 = thm "Abs_Up_inverse2";
+val Exh_Up = thm "Exh_Up";
+val inj_Abs_Up = thm "inj_Abs_Up";
+val inj_Rep_Up = thm "inj_Rep_Up";
+val inject_Iup = thm "inject_Iup";
+val defined_Iup = thm "defined_Iup";
+val upE = thm "upE";
+val Ifup1 = thm "Ifup1";
+val Ifup2 = thm "Ifup2";
+val less_up1a = thm "less_up1a";
+val less_up1b = thm "less_up1b";
+val less_up1c = thm "less_up1c";
+val refl_less_up = thm "refl_less_up";
+val antisym_less_up = thm "antisym_less_up";
+val trans_less_up = thm "trans_less_up";
+val inst_up_po = thm "inst_up_po";
+val minimal_up = thm "minimal_up";
+val UU_up_def = thm "UU_up_def";
+val least_up = thm "least_up";
+val less_up2b = thm "less_up2b";
+val less_up2c = thm "less_up2c";
+val monofun_Iup = thm "monofun_Iup";
+val monofun_Ifup1 = thm "monofun_Ifup1";
+val monofun_Ifup2 = thm "monofun_Ifup2";
+val up_lemma1 = thm "up_lemma1";
+val lub_up1a = thm "lub_up1a";
+val lub_up1b = thm "lub_up1b";
+val thelub_up1a = thm "thelub_up1a";
+val thelub_up1b = thm "thelub_up1b";
+val cpo_up = thm "cpo_up";
+val up_def = thm "up_def";
+val fup_def = thm "fup_def";
+val inst_up_pcpo = thm "inst_up_pcpo";
+val less_up3b = thm "less_up3b";
+val defined_Iup2 = thm "defined_Iup2";
+val contlub_Iup = thm "contlub_Iup";
+val cont_Iup = thm "cont_Iup";
+val contlub_Ifup1 = thm "contlub_Ifup1";
+val contlub_Ifup2 = thm "contlub_Ifup2";
+val cont_Ifup1 = thm "cont_Ifup1";
+val cont_Ifup2 = thm "cont_Ifup2";
+val Exh_Up1 = thm "Exh_Up1";
+val inject_up = thm "inject_up";
+val defined_up = thm "defined_up";
+val upE1 = thm "upE1";
+val fup1 = thm "fup1";
+val fup2 = thm "fup2";
+val less_up4b = thm "less_up4b";
+val less_up4c = thm "less_up4c";
+val thelub_up2a = thm "thelub_up2a";
+val thelub_up2b = thm "thelub_up2b";
+val up_lemma2 = thm "up_lemma2";
+val thelub_up2a_rev = thm "thelub_up2a_rev";
+val thelub_up2b_rev = thm "thelub_up2b_rev";
+val thelub_up3 = thm "thelub_up3";
+val fup3 = thm "fup3";