# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259749840 -3600
# Node ID 7fbbb2690bc585a8640eb71fd89560a058e87adb
# Parent  24799397a3ce628309e55ff95ec82de0ea7ebb5e
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.

diff -r 24799397a3ce -r 7fbbb2690bc5 FSet.thy
--- a/FSet.thy	Wed Dec 02 10:56:35 2009 +0100
+++ b/FSet.thy	Wed Dec 02 11:30:40 2009 +0100
@@ -371,7 +371,6 @@
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* C *) (* = and extensionality *)
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *)
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
@@ -380,22 +379,22 @@
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 7 *) (* respectfulness *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 7 *) (* respectfulness *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 done
 
 quotient_def
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
 
diff -r 24799397a3ce -r 7fbbb2690bc5 QuotMain.thy
--- a/QuotMain.thy	Wed Dec 02 10:56:35 2009 +0100
+++ b/QuotMain.thy	Wed Dec 02 11:30:40 2009 +0100
@@ -840,21 +840,36 @@
 
 *}
 
-
-
+definition
+  "QUOT_TRUE x \<equiv> True"
 
 ML {*
-fun APPLY_RSP_TAC rty = 
-  Subgoal.FOCUS (fn {concl, ...} =>
-    case HOLogic.dest_Trueprop (term_of concl) of
-       (_ $ (f $ _) $ (_ $ _)) =>
+fun find_qt_asm asms =
+  let
+    fun find_fun trm =
+      case trm of
+        (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true
+      | _ => false
+  in
+    case find_first find_fun asms of
+      SOME (_ $ (_ $ (f $ a))) => (f, a)
+    | _ => error "find_qt_asm"
+  end
+*}
+
+ML {*
+fun APPLY_RSP_TAC rty =
+  Subgoal.FOCUS (fn {concl, asms, ...} =>
+    case ((HOLogic.dest_Trueprop (term_of concl))) of
+       ((_ $ (f $ _) $ (_ $ _))) =>
           let
+            val (asmf, asma) = find_qt_asm (map term_of asms);
             val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
             val insts = Thm.match (pat, concl)
           in
-            if needs_lift rty (fastype_of f) 
-            then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
-            else no_tac
+            if (fastype_of asmf) = (fastype_of f)
+            then no_tac
+            else rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
           end
      | _ => no_tac)
 *}
@@ -886,9 +901,6 @@
 
 *)
 
-definition 
-  "QUOT_TRUE x \<equiv> True"
-
 lemma quot_true_dests:
   shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
   and   QT_ex:  "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
@@ -942,7 +954,7 @@
 ML {* fun unlam (Abs a) = snd (Term.dest_abs a) *}
 
 ML {*
-fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =
+fun inj_repabs_tac_old ctxt rty quot_thms rel_refl trans2 =
   (FIRST' [
     (* "cong" rule of the of the relation / transitivity*)
     (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
@@ -998,11 +1010,11 @@
 *}
 
 ML {*
-fun inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 =
+fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =
   (FIRST' [
     (* "cong" rule of the of the relation / transitivity*)
     (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
-    DT ctxt "1" (resolve_tac trans2),
+    NDT ctxt "1" (resolve_tac trans2),
 
     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
     NDT ctxt "2" (lambda_rsp_tac THEN' quot_true_tac ctxt unlam),