diff -r 114064363ef0 -r e2dc11e12e0b Closures2.thy
--- a/Closures2.thy	Sun Sep 04 07:28:48 2011 +0000
+++ b/Closures2.thy	Mon Sep 05 12:07:16 2011 +0000
@@ -1,4 +1,4 @@
-theory Closure2
+theory Closures2
 imports 
   Closures
   Higman
@@ -29,6 +29,7 @@
 
 hide_const A
 hide_const B
+hide_const R
 
 (*
 inductive 
@@ -255,14 +256,12 @@
 definition
   minimal :: "letter list \<Rightarrow> letter lang \<Rightarrow> bool"
 where
-  "minimal x A = (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)"
+  "minimal x A \<equiv> (\<forall>y \<in> A. y \<preceq> x \<longrightarrow> x \<preceq> y)"
 
 lemma main_lemma:
-  shows "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M"
+  shows "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M"
 proof -
   def M \<equiv> "{x \<in> A. minimal x A}"
-  have "M \<subseteq> A" unfolding M_def minimal_def by auto
-  moreover
   have "finite M"
     unfolding M_def minimal_def
     by (rule Higman_antichains) (auto simp add: emb_antisym)
@@ -278,14 +277,14 @@
     then have "z \<in> M"
       unfolding M_def minimal_def
       by (auto intro: emb_trans)
-    with b show "x \<in> SUPSEQ M"
+    with b(2) show "x \<in> SUPSEQ M"
       by (auto simp add: SUPSEQ_def)
   qed
   moreover
   have "SUPSEQ M \<subseteq> SUPSEQ A"
     by (auto simp add: SUPSEQ_def M_def)
   ultimately
-  show "\<exists>M. M \<subseteq> A \<and> finite M \<and> SUPSEQ A = SUPSEQ M" by blast
+  show "\<exists>M. finite M \<and> SUPSEQ A = SUPSEQ M" by blast
 qed
 
 lemma closure_SUPSEQ: