diff -r 020e27417b59 -r 0911d3aabf47 LFex.thy
--- a/LFex.thy	Mon Nov 30 12:14:20 2009 +0100
+++ b/LFex.thy	Mon Nov 30 15:32:14 2009 +0100
@@ -461,35 +461,7 @@
 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 {* clean_tac @{context} quot defs aps 1 *}) *)
-apply (tactic {* lambda_prs_tac @{context} quot 1 *})
-apply (tactic {* simp_tac ((Simplifier.context @{context} empty_ss) addsimps (meta_reps_same @ meta_lower)) 1 *})
-apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
-ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *}
-ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *}
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
-apply (tactic {* REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<longrightarrow>"]}) 1 *})
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
+apply(tactic {* clean_tac @{context} quot defs aps 1 *})
 done
 
 (* Does not work: