--- a/IntEx.thy	Sat Dec 05 22:16:17 2009 +0100
+++ b/IntEx.thy	Sat Dec 05 22:38:42 2009 +0100
@@ -154,10 +154,12 @@
 abbreviation 
   "Resp \<equiv> Respects"
 
+
 lemma "PLUS a b = PLUS a b"
 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* simp_tac (HOL_basic_ss addSolver quotient_solver addsimps @{thms all_prs})  1 *})
 apply(tactic {* clean_tac @{context} 1 *}) 
 done