--- 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 *})