diff -r 37285ec4387d -r e9e205b904e2 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Sun Dec 20 00:53:35 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Mon Dec 21 22:36:31 2009 +0100
@@ -249,7 +249,10 @@
 apply(lifting lam_tst3a)
 apply(rule impI)
 apply(rule lam_tst3a_reg)
-done
+apply(injection)
+sorry
+(* PROBLEM 
+done*)
 
 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"
 by auto
@@ -259,7 +262,10 @@
 apply(rule impI)
 apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
 apply(simp add: id_rsp)
-done
+apply(injection)
+sorry
+(* PROBLEM 
+done*)
 
 term map