--- a/Myhill_1.thy	Wed Feb 09 04:50:18 2011 +0000
+++ b/Myhill_1.thy	Wed Feb 09 04:54:23 2011 +0000
@@ -512,10 +512,6 @@
 definition 
   "ardenable ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> rhs_nonempty rhs"
 
-(* The following non_empty seems useless. *)
-definition 
-  "non_empty ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> X \<noteq> {}"
-
 text {* 
   @{text "finite_rhs ES"} requires every equation in @{text "rhs"} 
   be finite.
@@ -551,7 +547,7 @@
   *}
 definition 
   "invariant ES \<equiv> valid_eqns ES \<and> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> 
-                non_empty ES \<and> finite_rhs ES \<and> self_contained ES"
+                  finite_rhs ES \<and> self_contained ES"
 
 subsection {* The proof of this direction *}
 
@@ -748,8 +744,6 @@
     by (auto simp add:ardenable_def eqs_def init_rhs_def rhs_nonempty_def del:L_rhs.simps)
   moreover have "valid_eqns (eqs (UNIV // (\<approx>Lang)))"
     using l_eq_r_in_eqs by (simp add:valid_eqns_def)
-  moreover have "non_empty (eqs (UNIV // (\<approx>Lang)))"
-    by (auto simp:non_empty_def eqs_def quotient_def Image_def str_eq_rel_def)
   moreover have "finite_rhs (eqs (UNIV // (\<approx>Lang)))"
     using finite_init_rhs[OF finite_CS] 
     by (auto simp:finite_rhs_def eqs_def)
@@ -983,9 +977,6 @@
               subst_op_all_def subst_op_keeps_eq invariant_def finite_rhs_def
                    simp del:L_rhs.simps)
   qed
-  moreover have 
-    non_empty_subst: "non_empty (subst_op_all ES Y (arden_op Y yrhs))"
-    using invariant_ES by (auto simp:invariant_def non_empty_def subst_op_all_def)
   moreover 
   have self_subst: "self_contained (subst_op_all ES Y (arden_op Y yrhs))"
     using invariant_ES subst_op_all_keeps_self_contained by (simp add:invariant_def)