--- a/IntEx.thy	Sat Dec 05 21:45:39 2009 +0100
+++ b/IntEx.thy	Sat Dec 05 21:50:31 2009 +0100
@@ -178,7 +178,6 @@
 apply(simp only: in_respects)
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
-apply(simp only: Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
 done
 
 lemma test3: "my_plus = my_plus"
@@ -190,39 +189,13 @@
 apply(rule ho_plus_rsp)
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
-apply(simp only: Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int fun_quotient[OF Quotient_my_int Quotient_my_int]]])
 done
 
 
 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
 
@@ -272,7 +245,8 @@
 apply(simp only: Quotient_abs_rep[OF list_quotient[OF Quotient_my_int]])
 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
 apply(tactic {* clean_tac @{context} 1 *})
-sorry
+apply(simp) (* FIXME: why is this needed *)
+done
 
 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
 sorry

--- a/QuotMain.thy	Sat Dec 05 21:45:39 2009 +0100
+++ b/QuotMain.thy	Sat Dec 05 21:50:31 2009 +0100
@@ -1139,25 +1139,31 @@
  The rest are a simp_tac and are fast.
 *)
 
+ML {* fun OF1 thm1 thm2 = thm2 RS thm1 *}
+ML {*
+fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
+val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
+*}
+
 ML {*
 fun clean_tac lthy =
   let
     val thy = ProofContext.theory_of lthy;
-    val quotients = quotient_rules_get lthy
-    val defs = map (Thm.varifyT o #def) (qconsts_dest thy);
-    val absrep = map (fn x => @{thm Quotient_abs_rep} OF [x]) quotients
-    val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quotients
-    val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps
-      (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ absrep @ reps_same @ defs)
+    val defs = map (Thm.varifyT o #def) (qconsts_dest thy)
+    val thms = @{thms eq_reflection[OF fun_map.simps]} 
+               @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} 
+               @ defs
+    val simp_ctxt = HOL_basic_ss addsimps thms addSolver quotient_solver
   in
     EVERY' [
-      (* (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))  ---->  f *)
-      (* \<forall>x\<in>Respects R. (abs ---> id) f  ---->  \<forall>x. f *)
+      (* (rep1 ---> abs2) (\<lambda>x. rep2 (f (abs1 x)))  ---->  f *)
+      (* Ball (Respects R) ((abs ---> id) f)  ---->  All f *)
       NDT lthy "a" (TRY o lambda_allex_prs_tac lthy),
 
-      (* NewConst  ---->  (rep ---> abs) oldConst *)
-      (* Abs (Rep x)  ---->  x                    *)
-      (* id_simps; fun_map.simps                  *)
+      (* NewConst  ----->  (rep ---> abs) oldConst *)
+      (* abs (rep x)  ----->  x                    *)
+      (* R (Rep x) (Rep y) -----> x = y            *)
+      (* id_simps; fun_map.simps                   *)
       NDT lthy "c" (TRY o simp_tac simp_ctxt),
 
       (* final step *)