--- a/thys/LexerExt.thy	Sat Jul 01 13:08:48 2017 +0100
+++ b/thys/LexerExt.thy	Tue Jul 04 15:59:31 2017 +0100
@@ -362,6 +362,7 @@
 apply(auto)
 using Der_UNION Der_star Star_def by fastforce
 
+
 lemma ders_correctness:
   shows "L (ders s r) = Ders s (L r)"
 apply(induct s arbitrary: r)