--- a/thys/LexerExt.thy	Thu Mar 02 12:39:27 2017 +0000
+++ b/thys/LexerExt.thy	Sat Mar 04 21:35:12 2017 +0000
@@ -62,16 +62,16 @@
 unfolding Der_def
 by auto
 
+lemma Der_Sequ [simp]:
+  shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"
+unfolding Der_def Sequ_def
+by (auto simp add: Cons_eq_append_conv)
+
 lemma Der_union [simp]:
   shows "Der c (A \<union> B) = Der c A \<union> Der c B"
 unfolding Der_def
 by auto
 
-lemma Der_Sequ [simp]:
-  shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"
-unfolding Der_def Sequ_def
-by (auto simp add: Cons_eq_append_conv)
-
 lemma Der_UNION: 
   shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))"
 by (auto simp add: Der_def)