13 val recs = thms "lift.recs"; |
13 val recs = thms "lift.recs"; |
14 val simps = thms "lift.simps"; |
14 val simps = thms "lift.simps"; |
15 val size = thms "lift.size"; |
15 val size = thms "lift.size"; |
16 end; |
16 end; |
17 |
17 |
|
18 val cont2cont_flift1 = thm "cont2cont_flift1"; |
|
19 val cont2cont_lift_case = thm "cont2cont_lift_case"; |
|
20 val cont_flift1 = thm "cont_flift1"; |
|
21 val cont_lemmas_ext = thms "cont_lemmas_ext"; |
|
22 val cont_lift_case1 = thm "cont_lift_case1"; |
|
23 val cont_lift_case2 = thm "cont_lift_case2"; |
|
24 val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app"; |
|
25 val cont_Rep_CFun_app = thm "cont_Rep_CFun_app"; |
|
26 val DefE2 = thm "DefE2"; |
|
27 val DefE = thm "DefE"; |
|
28 val Def_inject_less_eq = thm "Def_inject_less_eq"; |
|
29 val Def_inject = thm "Def_inject"; |
|
30 val Def_less_is_eq = thm "Def_less_is_eq"; |
18 val Def_not_UU = thm "Def_not_UU"; |
31 val Def_not_UU = thm "Def_not_UU"; |
19 val DefE = thm "DefE"; |
32 val flift1_def = thm "flift1_def"; |
20 val DefE2 = thm "DefE2"; |
|
21 val Def_inject_less_eq = thm "Def_inject_less_eq"; |
|
22 val Def_less_is_eq = thm "Def_less_is_eq"; |
|
23 val Lift_cases = thm "Lift_cases"; |
|
24 val Lift_exhaust = thm "Lift_exhaust"; |
|
25 val cont_Rep_CFun_app = thm "cont_Rep_CFun_app"; |
|
26 val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app"; |
|
27 val cont_if = thm "cont_if"; |
|
28 val flift1_Def = thm "flift1_Def"; |
33 val flift1_Def = thm "flift1_Def"; |
29 val flift1_strict = thm "flift1_strict"; |
34 val flift1_strict = thm "flift1_strict"; |
30 val flift1_def = thm "flift1_def"; |
35 val flift2_defined = thm "flift2_defined"; |
|
36 val flift2_def = thm "flift2_def"; |
31 val flift2_Def = thm "flift2_Def"; |
37 val flift2_Def = thm "flift2_Def"; |
32 val flift2_strict = thm "flift2_strict"; |
38 val flift2_strict = thm "flift2_strict"; |
33 val flift2_def = thm "flift2_def"; |
39 val inst_lift_pcpo = thm "inst_lift_pcpo"; |
34 val flift2_defined = thm "flift2_defined"; |
40 val less_lift_def = thm "less_lift_def"; |
35 val less_lift = thm "less_lift"; |
41 val less_lift = thm "less_lift"; |
36 val less_lift_def = thm "less_lift_def"; |
42 val Lift_cases = thm "Lift_cases"; |
|
43 val lift_definedE = thm "lift_definedE"; |
|
44 val lift_distinct1 = thm "lift_distinct1"; |
|
45 val lift_distinct2 = thm "lift_distinct2"; |
|
46 val Lift_exhaust = thm "Lift_exhaust"; |
|
47 val lift_induct = thm "lift_induct"; |
37 val liftpair_def = thm "liftpair_def"; |
48 val liftpair_def = thm "liftpair_def"; |
38 val not_Undef_is_Def = thm "not_Undef_is_Def"; |
49 val not_Undef_is_Def = thm "not_Undef_is_Def"; |