--- a/More_Regular_Set.thy	Tue Jul 26 10:58:26 2011 +0000
+++ b/More_Regular_Set.thy	Tue Jul 26 18:12:07 2011 +0000
@@ -34,13 +34,13 @@
 using a
 by (induct rule: star_induct) (blast)+
 
-lemma seq_pow_comm:
+lemma conc_pow_comm:
   shows "A \<cdot> (A ^^ n) = (A ^^ n) \<cdot> A"
 by (induct n) (simp_all add: conc_assoc[symmetric])
 
-lemma seq_star_comm:
+lemma conc_star_comm:
   shows "A \<cdot> A\<star> = A\<star> \<cdot> A"
-unfolding star_def seq_pow_comm conc_UNION_distrib
+unfolding star_def conc_pow_comm conc_UNION_distrib
 by simp
 
 
@@ -68,13 +68,13 @@
     by (simp only: length_append)
 qed
 
-lemma seq_pow_length:
+lemma conc_pow_length:
   assumes a: "[] \<notin> A"
   and     b: "s \<in> B \<cdot> (A ^^ Suc n)"
   shows "n < length s"
 proof -
   from b obtain s1 s2 where eq: "s = s1 @ s2" and *: "s2 \<in> A ^^ Suc n"
-    unfolding Seq_def by auto
+    by auto
   from * have " n < length s2" by (rule pow_length[OF a])
   then show "n < length s" using eq by simp
 qed
@@ -108,7 +108,7 @@
 proof
   assume eq: "X = B \<cdot> A\<star>"
   have "A\<star> = {[]} \<union> A\<star> \<cdot> A" 
-    unfolding seq_star_comm[symmetric]
+    unfolding conc_star_comm[symmetric]
     by (rule star_cases)
   then have "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)"
     by (rule conc_add_left)
@@ -128,7 +128,7 @@
   { fix s::"'a list"
     obtain k where "k = length s" by auto
     then have not_in: "s \<notin> X \<cdot> (A ^^ Suc k)" 
-      using seq_pow_length[OF nemp] by blast
+      using conc_pow_length[OF nemp] by blast
     assume "s \<in> X"
     then have "s \<in> X \<cdot> (A ^^ Suc k) \<union> (\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m))"
       using arden_helper[OF eq, of "k"] by auto