diff -r 6ce4f274b0fa -r ca37f4b6457c Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Mon Dec 07 21:25:49 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 11:17:56 2009 +0100
@@ -308,6 +308,20 @@
 lemma lam_tst3a: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
 by auto
 
+lemma lam_tst3a_clean: "(op \<approx> ===> op \<approx>)
+     ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (Babs (Respects op \<approx>) (
+       ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (\<lambda>y. REP_my_int (ABS_my_int y))))))))
+     ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (Babs (Respects op \<approx>) (
+       ((ABS_my_int ---> REP_my_int) ((REP_my_int ---> ABS_my_int) (\<lambda>y. REP_my_int (ABS_my_int y))))))))
+      = ((\<lambda>(y::my_int). y) = (\<lambda>x. x))"
+apply(subst babs_prs[OF Quotient_my_int Quotient_my_int])
+apply(subst babs_prs[OF Quotient_my_int Quotient_my_int])
+apply(subst lambda_prs[OF Quotient_my_int Quotient_my_int])
+apply(subst lambda_prs[OF Quotient_my_int Quotient_my_int])
+apply(subst Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
+apply(rule refl)
+done
+
 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *})
 defer
@@ -337,4 +351,4 @@
 apply(tactic {* regularize_tac @{context} 1*})?
 sorry
 
-end
\ No newline at end of file
+end