--- a/src/HOLCF/Up.ML Wed Jun 08 00:59:46 2005 +0200
+++ b/src/HOLCF/Up.ML Wed Jun 08 01:40:39 2005 +0200
@@ -4,59 +4,28 @@
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 up_inject = thm "up_inject";
+val up_eq = thm "up_eq";
+val up_defined = thm "up_defined";
+val up_less = thm "up_less";
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";