equal
deleted
inserted
replaced
265 apply - |
265 apply - |
266 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
266 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
267 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
267 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
268 prefer 2 |
268 prefer 2 |
269 apply(tactic {* clean_tac @{context} quot defs 1 *}) |
269 apply(tactic {* clean_tac @{context} quot defs 1 *}) |
270 apply(tactic {* all_inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*}) |
270 apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1*}) |
271 done |
271 done |
272 |
272 |
273 (* Does not work: |
273 (* Does not work: |
274 lemma |
274 lemma |
275 assumes a0: "P1 TYP" |
275 assumes a0: "P1 TYP" |
294 \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2); |
294 \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2); |
295 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
295 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
296 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
296 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
297 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
297 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
298 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
298 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
299 apply(tactic {* all_inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *}) |
299 apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *}) |
300 apply(tactic {* clean_tac @{context} quot defs 1 *}) |
300 apply(tactic {* clean_tac @{context} quot defs 1 *}) |
301 done |
301 done |
302 |
302 |
303 print_quotients |
303 print_quotients |
304 |
304 |