# HG changeset patch
# User urbanc
# Date 1315095701 0
# Node ID 999fce5f9d34d99aed7a93051d63cc5ff7a91a8c
# Parent  6bb8ad9093e67011537363dcdbaf448b7af93ec1
removed the last two sorry's

diff -r 6bb8ad9093e6 -r 999fce5f9d34 Closures2.thy
--- a/Closures2.thy	Fri Sep 02 14:29:54 2011 +0000
+++ b/Closures2.thy	Sun Sep 04 00:21:41 2011 +0000
@@ -245,9 +245,9 @@
   from higman_idx obtain i j where d: "i < j" and e: "f i \<preceq> f j" by blast
   have "f i \<noteq> f j" using b d by (auto simp add: inj_on_def)
   moreover
-  have "f i \<in> A" sorry
+  have "f i \<in> A" using c by auto
   moreover
-  have "f j \<in> A" sorry
+  have "f j \<in> A" using c by auto
   ultimately have "\<not>(f i \<preceq> f j)" using a by simp
   with e show "False" by simp
 qed