equal
deleted
inserted
replaced
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 cont_Rep_CFun_app = thm "cont_Rep_CFun_app"; |
25 val cont_Rep_CFun_app = thm "cont_Rep_CFun_app"; |
26 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"; |
27 val cont_flift1_arg = thm "cont_flift1_arg"; |
|
28 val cont_flift1_arg_and_not_arg = thm "cont_flift1_arg_and_not_arg"; |
|
29 val cont_flift1_not_arg = thm "cont_flift1_not_arg"; |
|
30 (*val cont_flift2_arg = thm "cont_flift2_arg";*) |
|
31 val cont_if = thm "cont_if"; |
27 val cont_if = thm "cont_if"; |
32 val flift1_Def = thm "flift1_Def"; |
28 val flift1_Def = thm "flift1_Def"; |
33 val flift1_strict = thm "flift1_strict"; |
29 val flift1_strict = thm "flift1_strict"; |
34 val flift1_def = thm "flift1_def"; |
30 val flift1_def = thm "flift1_def"; |
35 val flift2_Def = thm "flift2_Def"; |
31 val flift2_Def = thm "flift2_Def"; |