diff -r 5d932e7a856c -r e56eeb9fedb3 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Mon Dec 07 14:35:45 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Mon Dec 07 15:18:00 2009 +0100
@@ -256,13 +256,11 @@
 by simp
 
 
-
-
 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *})
 defer
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-(*apply(tactic {* lambda_prs_tac  @{context} 1 *})*)
+apply(tactic {* clean_tac  @{context} 1 *})
 sorry
 
 lemma lam_tst3: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"
@@ -272,5 +270,5 @@
 apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *})
 defer
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* lambda_prs_tac  @{context} 1 *})
+apply(tactic {* clean_tac  @{context} 1 *})
 sorry