20 val DefE2 = thm "DefE2"; |
20 val DefE2 = thm "DefE2"; |
21 val Def_inject_less_eq = thm "Def_inject_less_eq"; |
21 val Def_inject_less_eq = thm "Def_inject_less_eq"; |
22 val Def_less_is_eq = thm "Def_less_is_eq"; |
22 val Def_less_is_eq = thm "Def_less_is_eq"; |
23 val Lift_cases = thm "Lift_cases"; |
23 val Lift_cases = thm "Lift_cases"; |
24 val Lift_exhaust = thm "Lift_exhaust"; |
24 val Lift_exhaust = thm "Lift_exhaust"; |
25 val UU_lift_def = thm "UU_lift_def"; |
|
26 val Undef_eq_UU = thm "Undef_eq_UU"; |
|
27 val cont_Rep_CFun_app = thm "cont_Rep_CFun_app"; |
25 val cont_Rep_CFun_app = thm "cont_Rep_CFun_app"; |
28 val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app"; |
26 val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app"; |
29 val cont_flift1_arg = thm "cont_flift1_arg"; |
27 val cont_flift1_arg = thm "cont_flift1_arg"; |
30 val cont_flift1_arg_and_not_arg = thm "cont_flift1_arg_and_not_arg"; |
28 val cont_flift1_arg_and_not_arg = thm "cont_flift1_arg_and_not_arg"; |
31 val cont_flift1_not_arg = thm "cont_flift1_not_arg"; |
29 val cont_flift1_not_arg = thm "cont_flift1_not_arg"; |
32 val cont_flift2_arg = thm "cont_flift2_arg"; |
30 val cont_flift2_arg = thm "cont_flift2_arg"; |
33 val cont_if = thm "cont_if"; |
31 val cont_if = thm "cont_if"; |
34 val flat_imp_chfin_poo = thm "flat_imp_chfin_poo"; |
|
35 val flift1_Def = thm "flift1_Def"; |
32 val flift1_Def = thm "flift1_Def"; |
36 val flift1_strict = thm "flift1_strict"; |
33 val flift1_strict = thm "flift1_strict"; |
37 val flift1_def = thm "flift1_def"; |
34 val flift1_def = thm "flift1_def"; |
38 val flift2_Def = thm "flift2_Def"; |
35 val flift2_Def = thm "flift2_Def"; |
39 val flift2_strict = thm "flift2_strict"; |
36 val flift2_strict = thm "flift2_strict"; |
40 val flift2_def = thm "flift2_def"; |
37 val flift2_def = thm "flift2_def"; |
41 val flift2_defined = thm "flift2_defined"; |
38 val flift2_defined = thm "flift2_defined"; |
42 val inst_lift_pcpo = thm "inst_lift_pcpo"; |
|
43 val inst_lift_po = thm "inst_lift_po"; |
|
44 val least_lift = thm "least_lift"; |
|
45 val less_lift = thm "less_lift"; |
39 val less_lift = thm "less_lift"; |
46 val less_lift_def = thm "less_lift_def"; |
40 val less_lift_def = thm "less_lift_def"; |
47 val liftpair_def = thm "liftpair_def"; |
41 val liftpair_def = thm "liftpair_def"; |
48 val minimal_lift = thm "minimal_lift"; |
|
49 val not_Undef_is_Def = thm "not_Undef_is_Def"; |
42 val not_Undef_is_Def = thm "not_Undef_is_Def"; |