diff -r 00c9a95d492e -r e2828c4a1e23 thys/Lexer.thy
--- a/thys/Lexer.thy	Tue Jul 04 18:09:29 2017 +0100
+++ b/thys/Lexer.thy	Thu Jul 06 16:05:33 2017 +0100
@@ -85,6 +85,13 @@
 by (induct x\<equiv>"c # x" rule: Star.induct) 
    (auto simp add: append_eq_Cons_conv)
 
+lemma Star_Der_Sequ: 
+  shows "Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>"
+unfolding Der_def
+by(auto simp add: Der_def Sequ_def Star_decomp)
+
+
+
 lemma Der_star [simp]:
   shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
 proof -    
@@ -95,8 +102,7 @@
   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)
+    using Star_Der_Sequ by auto
   finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
 qed