--- a/src/HOLCF/Lift.ML Wed May 25 01:47:11 2005 +0200
+++ b/src/HOLCF/Lift.ML Wed May 25 02:49:46 2005 +0200
@@ -24,7 +24,6 @@
val Lift_exhaust = thm "Lift_exhaust";
val UU_lift_def = thm "UU_lift_def";
val Undef_eq_UU = thm "Undef_eq_UU";
-val chain_mono2_po = thm "chain_mono2_po";
val cont2cont_CF1L_rev2 = thm "cont2cont_CF1L_rev2";
val cont_Rep_CFun_app = thm "cont_Rep_CFun_app";
val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app";
@@ -33,7 +32,6 @@
val cont_flift1_not_arg = thm "cont_flift1_not_arg";
val cont_flift2_arg = thm "cont_flift2_arg";
val cont_if = thm "cont_if";
-val cpo_lift = thm "cpo_lift";
val flat_imp_chfin_poo = thm "flat_imp_chfin_poo";
val flift1_Def = thm "flift1_Def";
val flift1_UU = thm "flift1_UU";
@@ -49,5 +47,4 @@
val less_lift_def = thm "less_lift_def";
val liftpair_def = thm "liftpair_def";
val minimal_lift = thm "minimal_lift";
-val notUndef_I = thm "notUndef_I";
val not_Undef_is_Def = thm "not_Undef_is_Def";