equal
deleted
inserted
replaced
258 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
258 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
259 apply - |
259 apply - |
260 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
260 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
261 apply(tactic {* regularize_tac @{context} @{thms alpha_equivps} 1 *}) |
261 apply(tactic {* regularize_tac @{context} @{thms alpha_equivps} 1 *}) |
262 apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *}) |
262 apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *}) |
263 apply(fold perm_kind_def perm_ty_def perm_trm_def FV_ty_def[simplified id_simps] FV_kind_def[simplified id_simps] FV_trm_def[simplified id_simps]) |
263 apply(fold perm_kind_def perm_ty_def perm_trm_def) |
264 apply(tactic {* clean_tac @{context} 1 *}) |
264 apply(tactic {* clean_tac @{context} 1 *}) |
265 (* |
265 (* |
266 Profiling: |
266 Profiling: |
267 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
267 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
268 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |
268 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |