equal
deleted
inserted
replaced
296 \<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2); |
296 \<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2); |
297 \<And>id. P3 (CONS id); \<And>name. P3 (VAR name); |
297 \<And>id. P3 (CONS id); \<And>name. P3 (VAR name); |
298 \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2); |
298 \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2); |
299 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
299 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
300 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
300 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
301 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
301 apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_EQUIVs} quot 1 *}) |
302 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
|
303 apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *}) |
|
304 apply(tactic {* clean_tac @{context} quot 1 *}) |
|
305 done |
302 done |
306 |
303 |
307 print_quotients |
304 print_quotients |
308 |
305 |
309 end |
306 end |