--- a/thys/Lexer.thy	Wed Jun 28 10:37:05 2017 +0100
+++ b/thys/Lexer.thy	Thu Jun 29 17:57:41 2017 +0100
@@ -13,12 +13,12 @@
 
 text {* Two Simple Properties about Sequential Composition *}
 
-lemma seq_empty [simp]:
+lemma Sequ_empty_string [simp]:
   shows "A ;; {[]} = A"
   and   "{[]} ;; A = A"
 by (simp_all add: Sequ_def)
 
-lemma seq_null [simp]:
+lemma Sequ_empty [simp]:
   shows "A ;; {} = {}"
   and   "{} ;; A = {}"
 by (simp_all add: Sequ_def)
@@ -71,12 +71,14 @@
   start[intro]: "[] \<in> A\<star>"
 | step[intro]:  "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"
 
-lemma star_cases:
+(* Arden's lemma *)
+
+lemma Star_cases:
   shows "A\<star> = {[]} \<union> A ;; A\<star>"
 unfolding Sequ_def
 by (auto) (metis Star.simps)
 
-lemma star_decomp: 
+lemma Star_decomp: 
   assumes a: "c # x \<in> A\<star>" 
   shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"
 using a
@@ -87,14 +89,14 @@
   shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
 proof -    
   have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"  
-    by (simp only: star_cases[symmetric])
+    by (simp only: Star_cases[symmetric])
   also have "... = Der c (A ;; A\<star>)"
     by (simp only: Der_union Der_empty) (simp)
   also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})"
     by simp
   also have "... =  (Der c A) ;; A\<star>"
     unfolding Sequ_def Der_def
-    by (auto dest: star_decomp)
+    by (auto dest: Star_decomp)
   finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
 qed
 
@@ -291,12 +293,14 @@
 
 
 lemma L_flat_Prf1:
-  assumes "\<turnstile> v : r" shows "flat v \<in> L r"
+  assumes "\<turnstile> v : r" 
+  shows "flat v \<in> L r"
 using assms
 by (induct)(auto simp add: Sequ_def)
 
 lemma L_flat_Prf2:
-  assumes "s \<in> L r" shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"
+  assumes "s \<in> L r" 
+  shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"
 using assms
 apply(induct r arbitrary: s)
 apply(auto simp add: Sequ_def intro: Prf.intros)
@@ -324,7 +328,6 @@
 using assms
 apply(drule_tac Star_string)
 apply(auto)
-
 by (metis L_flat_Prf2 Prf_Stars Star_val)