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 UU_lift_def = thm "UU_lift_def"; |
25 val UU_lift_def = thm "UU_lift_def"; |
26 val Undef_eq_UU = thm "Undef_eq_UU"; |
26 val Undef_eq_UU = thm "Undef_eq_UU"; |
27 val cont2cont_CF1L_rev2 = thm "cont2cont_CF1L_rev2"; |
|
28 val cont_Rep_CFun_app = thm "cont_Rep_CFun_app"; |
27 val cont_Rep_CFun_app = thm "cont_Rep_CFun_app"; |
29 val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app"; |
28 val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app"; |
30 val cont_flift1_arg = thm "cont_flift1_arg"; |
29 val cont_flift1_arg = thm "cont_flift1_arg"; |
31 val cont_flift1_arg_and_not_arg = thm "cont_flift1_arg_and_not_arg"; |
30 val cont_flift1_arg_and_not_arg = thm "cont_flift1_arg_and_not_arg"; |
32 val cont_flift1_not_arg = thm "cont_flift1_not_arg"; |
31 val cont_flift1_not_arg = thm "cont_flift1_not_arg"; |