diff -r 97a397ba5743 -r fe2a37cfecd3 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Tue Dec 08 20:55:55 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 22:02:14 2009 +0100
@@ -204,8 +204,8 @@
 
 lemma "foldl PLUS x [] = x"
 apply(lifting ho_tst)
+apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
 apply(tactic {* clean_tac @{context} 1 *})
-apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
 done
 
 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
@@ -215,8 +215,8 @@
 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
 apply(tactic {* all_inj_repabs_tac @{context} 1*})
+apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int])
 apply(tactic {* clean_tac @{context} 1 *})
-apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int])
 done
 
 lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s"
@@ -226,10 +226,8 @@
 apply(tactic {* procedure_tac @{context} @{thm ho_tst3} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
 apply(tactic {* all_inj_repabs_tac @{context} 1*})
-(* TODO: does not work when this is added *)
-(* apply(tactic {* lambda_prs_tac @{context} 1 *})*)
+apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
 apply(tactic {* clean_tac @{context} 1 *})
-apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
 done
 
 lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))"
@@ -310,8 +308,8 @@
 apply(rule impI)
 apply(rule lam_tst3a_reg)
 apply(tactic {* all_inj_repabs_tac @{context} 1*})
+apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int])
 apply(tactic {* clean_tac  @{context} 1 *})
-apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int])
 done
 
 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"
@@ -344,9 +342,9 @@
 
 lemma "map (\<lambda>x. PLUS x ZERO) l = l"
 apply(lifting lam_tst4)
+apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int])
+apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int])
 apply(cleaning)
-apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int])
-apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int, symmetric])
 done
 
 end