diff -r 114bb544ecb9 -r d641c32855f0 IntEx.thy
--- a/IntEx.thy	Sat Dec 05 21:47:48 2009 +0100
+++ b/IntEx.thy	Sat Dec 05 21:50:31 2009 +0100
@@ -176,24 +176,7 @@
 apply(rule ballI)
 apply(rule apply_rsp[OF Quotient_my_int ho_plus_rsp])
 apply(simp only: in_respects)
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(rule quot_rel_rsp)
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(fold PLUS_def)
+apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
@@ -204,14 +187,7 @@
 lemma "PLUS = PLUS"
 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
 apply(rule ho_plus_rsp)
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(rule quot_rel_rsp)
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
@@ -219,32 +195,7 @@
 lemma "PLUS a b = PLUS b a"
 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done