equal
deleted
inserted
replaced
177 @{thms ho_all_prs ho_ex_prs} *} |
177 @{thms ho_all_prs ho_ex_prs} *} |
178 |
178 |
179 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
179 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
180 ML {* val consts = lookup_quot_consts defs *} |
180 ML {* val consts = lookup_quot_consts defs *} |
181 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
181 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
182 ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] rty [quot] trans2 rsp_thms defs *} |
182 ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *} |
183 |
183 |
184 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)" |
184 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)" |
185 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) |
185 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) |
186 done |
186 done |
187 |
187 |