diff -r 2480fb2a5e4e -r 5961edda27d7 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Tue Jan 12 10:59:51 2010 +0100
+++ b/Quot/Examples/IntEx.thy	Wed Jan 13 00:45:28 2010 +0100
@@ -252,7 +252,8 @@
 apply(lifting lam_tst3a)
 apply(rule impI)
 apply(rule lam_tst3a_reg)
-done
+(* INJECTION PROBLEM *)
+oops
 
 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
@@ -262,7 +263,8 @@
 apply(rule impI)
 apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
 apply(simp add: id_rsp)
-done
+(* INJECTION PROBLEM *)
+oops
 
 term map