equal
deleted
inserted
replaced
169 apply (simp_all add: rlam.inject alpha_refl) |
169 apply (simp_all add: rlam.inject alpha_refl) |
170 done |
170 done |
171 |
171 |
172 ML {* val qty = @{typ "lam"} *} |
172 ML {* val qty = @{typ "lam"} *} |
173 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *} |
173 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *} |
174 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @ |
174 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *} |
175 @{thms ho_all_prs ho_ex_prs} *} |
|
176 |
175 |
177 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
176 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
178 ML {* val consts = lookup_quot_consts defs *} |
177 ML {* val consts = lookup_quot_consts defs *} |
179 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
178 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
180 ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} |
179 ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} |