--- a/thys/Lexer.thy	Sat Jul 01 13:08:48 2017 +0100
+++ b/thys/Lexer.thy	Tue Jul 04 15:59:31 2017 +0100
@@ -171,6 +171,9 @@
 apply(simp_all add: Ders_def der_correctness Der_def)
 done
 
+
+section {* Lemmas about ders *}
+
 lemma ders_ZERO:
   shows "ders s (ZERO) = ZERO"
 apply(induct s)
@@ -184,8 +187,9 @@
 done
 
 lemma ders_CHAR:
-  shows "ders s (CHAR c) = (if s = [c] then ONE else 
-                           (if s = [] then (CHAR c) else ZERO))"
+  shows "ders s (CHAR c) = 
+           (if s = [c] then ONE else 
+           (if s = [] then (CHAR c) else ZERO))"
 apply(induct s)
 apply(simp_all add: ders_ZERO ders_ONE)
 done