equal
deleted
inserted
replaced
294 \<And>ty1 name ty2. \<lbrakk>Q ty1; Q ty2\<rbrakk> \<Longrightarrow> Q (TPI ty1 name ty2); |
294 \<And>ty1 name ty2. \<lbrakk>Q ty1; Q ty2\<rbrakk> \<Longrightarrow> Q (TPI ty1 name ty2); |
295 \<And>id. R (CONS id); \<And>name. R (VAR name); |
295 \<And>id. R (CONS id); \<And>name. R (VAR name); |
296 \<And>trm1 trm2. \<lbrakk>R trm1; R trm2\<rbrakk> \<Longrightarrow> R (APP trm1 trm2); |
296 \<And>trm1 trm2. \<lbrakk>R trm1; R trm2\<rbrakk> \<Longrightarrow> R (APP trm1 trm2); |
297 \<And>ty name trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> R (LAM ty name trm)\<rbrakk> |
297 \<And>ty name trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> R (LAM ty name trm)\<rbrakk> |
298 \<Longrightarrow> P mkind \<and> Q mty \<and> R mtrm" |
298 \<Longrightarrow> P mkind \<and> Q mty \<and> R mtrm" |
299 apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_equivps} 1 *}) |
299 apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
300 done |
300 done |
301 |
301 |
302 print_quotients |
302 print_quotients |
303 |
303 |
304 end |
304 end |