Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
LFex.thy
changeset 445 f1c0a66284d3
parent 441 42e7f323913a
child 446 84ee3973f083 
--- a/LFex.thy	Sat Nov 28 14:15:05 2009 +0100
+++ b/LFex.thy	Sat Nov 28 14:33:04 2009 +0100
@@ -269,197 +269,197 @@
   val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs}
   val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs}
 *}
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp fv_ty_rsp fv_kind_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tconst_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tpi_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms perm_ty_rsp tpi_rsp fv_ty_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms const_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms var_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms app_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms lam_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_trm_rsp lam_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp fv_ty_rsp fv_kind_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tconst_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tpi_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms perm_ty_rsp tpi_rsp fv_ty_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms const_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms var_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms app_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms lam_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_trm_rsp lam_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 []) 1*})
 done
 
 print_quotients
nominal2