--- a/IntEx.thy	Sat Dec 05 22:38:42 2009 +0100
+++ b/IntEx.thy	Sat Dec 05 23:26:08 2009 +0100
@@ -159,7 +159,6 @@
 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
 
@@ -214,22 +213,6 @@
 apply simp
 done
 
-(* I believe it's true. *)
-lemma foldl_rsp[quotient_rsp]:
-  "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> list_rel op \<approx> ===> op \<approx>) foldl foldl"
-apply (simp only: fun_rel.simps)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
-apply (induct_tac xb yb rule: list_induct2) (* To finish I need to give it: arbitrary:xa ya *)
-sorry
-
 lemma "foldl PLUS x [] = x"
 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})