# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260268738 -3600
# Node ID a98b136fc88aacc38bd455b920b3dbfd508e939b
# Parent  faab2540f13e4b8fbfd7e13f3ed6fc9db1bbc05a
It also regularizes.

diff -r faab2540f13e -r a98b136fc88a Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Tue Dec 08 11:28:04 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 11:38:58 2009 +0100
@@ -323,6 +323,15 @@
 apply(tactic {* all_inj_repabs_tac @{context} 1*})
 done
 
+lemma id_rsp:
+  shows "(R ===> R) id id"
+by simp
+
+lemma lam_tst3a_reg: "(op \<approx> ===> op \<approx>) (Babs (Respects op \<approx>) (\<lambda>y. y)) (Babs (Respects op \<approx>) (\<lambda>x. x))"
+apply (rule babs_rsp[OF Quotient_my_int])
+apply (simp add: id_rsp)
+done
+
 
 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *})