diff -r 24799397a3ce -r 7fbbb2690bc5 LFex.thy
--- a/LFex.thy	Wed Dec 02 10:56:35 2009 +0100
+++ b/LFex.thy	Wed Dec 02 11:30:40 2009 +0100
@@ -225,8 +225,6 @@
   val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM}
   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}
-  val lower = flat (map (add_lower_defs @{context}) defs)
-  val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower
   val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
   val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
 *}
@@ -267,198 +265,9 @@
 apply - 
 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 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 {* all_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 {* all_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 {* all_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 {* all_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 {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
-apply(tactic {* all_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 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 {* all_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 {* all_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 {* all_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 {* all_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 {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* all_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 {* all_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 {* 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 {* all_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 {* all_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 {* all_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 {* all_inj_repabs_tac @{context} @{typ trm} 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 {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* all_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 {* all_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 {* all_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 {* all_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 {* all_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 {* all_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 {* 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 {* all_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 {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
-apply(tactic {* all_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 {* 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 {* all_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 {* all_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 {* all_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 {* all_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 {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* all_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 {* all_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 {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2  1*})
+prefer 2
 apply(tactic {* clean_tac @{context} quot defs 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
 done
 
 (* Does not work:
@@ -487,97 +296,7 @@
   \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm"
 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 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 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 {* all_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 {* 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 {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* all_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 {* all_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 {* 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 {* all_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 {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
-apply(tactic {* all_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 {* all_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 {* all_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 {* all_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 {* all_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 {* 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 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 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 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 *})
-(* LOOP! *)
-(* apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) *)
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* all_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 {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
 apply(tactic {* clean_tac @{context} quot defs 1 *})
 done