diff -r 0384e039b7f2 -r e121ac0028f8 IntEx.thy
--- a/IntEx.thy	Sun Dec 06 00:13:35 2009 +0100
+++ b/IntEx.thy	Sun Dec 06 00:19:45 2009 +0100
@@ -162,7 +162,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
 
@@ -217,22 +216,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 *})