diff -r b3bb2bad952f -r 129caba33c03 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Sat Jan 09 09:38:34 2010 +0100
+++ b/Quot/Examples/IntEx.thy	Mon Jan 11 00:31:29 2010 +0100
@@ -250,10 +250,7 @@
 apply(lifting lam_tst3a)
 apply(rule impI)
 apply(rule lam_tst3a_reg)
-apply(injection)
-sorry
-(* PROBLEM 
-done*)
+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
@@ -263,10 +260,7 @@
 apply(rule impI)
 apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
 apply(simp add: id_rsp)
-apply(injection)
-sorry
-(* PROBLEM 
-done*)
+done
 
 term map