equal
deleted
inserted
replaced
82 (rtac (Abs_Lift_inverse RS ssubst) 1), |
82 (rtac (Abs_Lift_inverse RS ssubst) 1), |
83 (rtac (sum_case_Inr RS ssubst) 1), |
83 (rtac (sum_case_Inr RS ssubst) 1), |
84 (rtac refl 1) |
84 (rtac refl 1) |
85 ]); |
85 ]); |
86 |
86 |
87 val Lift_ss = Cfun_ss addsimps [Ilift1,Ilift2]; |
87 Addsimps [Ilift1,Ilift2]; |
88 |
88 |
89 qed_goalw "less_lift1a" Lift1.thy [less_lift_def,UU_lift_def] |
89 qed_goalw "less_lift1a" Lift1.thy [less_lift_def,UU_lift_def] |
90 "less_lift(UU_lift)(z)" |
90 "less_lift(UU_lift)(z)" |
91 (fn prems => |
91 (fn prems => |
92 [ |
92 [ |