# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260267601 -3600
# Node ID 8dfae5d97387e035e0524663afdd962c39eff52d
# Parent  ca37f4b6457c26f2139686ae0d31b8ab2de3d422# Parent  20b8585ad1e0c1e7d7eb09499f85a18d432fca7d
merge

diff -r 20b8585ad1e0 -r 8dfae5d97387 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Tue Dec 08 04:21:14 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 11:20:01 2009 +0100
@@ -299,6 +299,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
@@ -328,4 +342,4 @@
 apply(tactic {* regularize_tac @{context} 1*})?
 sorry
 
-end
\ No newline at end of file
+end