src/HOLCF/Lift.ML

--- a/src/HOLCF/Lift.ML	Tue Jul 26 18:28:11 2005 +0200
+++ b/src/HOLCF/Lift.ML	Tue Jul 26 18:29:59 2005 +0200
@@ -15,24 +15,35 @@
   val size = thms "lift.size";
 end;
 
-val Def_not_UU = thm "Def_not_UU";
+val cont2cont_flift1 = thm "cont2cont_flift1";
+val cont2cont_lift_case = thm "cont2cont_lift_case";
+val cont_flift1 = thm "cont_flift1";
+val cont_lemmas_ext = thms "cont_lemmas_ext";
+val cont_lift_case1 = thm "cont_lift_case1";
+val cont_lift_case2 = thm "cont_lift_case2";
+val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app";
+val cont_Rep_CFun_app = thm "cont_Rep_CFun_app";
+val DefE2 = thm "DefE2";
 val DefE = thm "DefE";
-val DefE2 = thm "DefE2";
 val Def_inject_less_eq = thm "Def_inject_less_eq";
+val Def_inject = thm "Def_inject";
 val Def_less_is_eq = thm "Def_less_is_eq";
-val Lift_cases = thm "Lift_cases";
-val Lift_exhaust = thm "Lift_exhaust";
-val cont_Rep_CFun_app = thm "cont_Rep_CFun_app";
-val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app";
-val cont_if = thm "cont_if";
+val Def_not_UU = thm "Def_not_UU";
+val flift1_def = thm "flift1_def";
 val flift1_Def = thm "flift1_Def";
 val flift1_strict = thm "flift1_strict";
-val flift1_def = thm "flift1_def";
+val flift2_defined = thm "flift2_defined";
+val flift2_def = thm "flift2_def";
 val flift2_Def = thm "flift2_Def";
 val flift2_strict = thm "flift2_strict";
-val flift2_def = thm "flift2_def";
-val flift2_defined = thm "flift2_defined";
+val inst_lift_pcpo = thm "inst_lift_pcpo";
+val less_lift_def = thm "less_lift_def";
 val less_lift = thm "less_lift";
-val less_lift_def = thm "less_lift_def";
+val Lift_cases = thm "Lift_cases";
+val lift_definedE = thm "lift_definedE";
+val lift_distinct1 = thm "lift_distinct1";
+val lift_distinct2 = thm "lift_distinct2";
+val Lift_exhaust = thm "Lift_exhaust";
+val lift_induct = thm "lift_induct";
 val liftpair_def = thm "liftpair_def";
 val not_Undef_is_Def = thm "not_Undef_is_Def";