diff -r c090baa7059d -r 8b8db9558ecf thys/Lexer.thy
--- a/thys/Lexer.thy	Mon Feb 11 23:18:05 2019 +0000
+++ b/thys/Lexer.thy	Sun Feb 17 22:15:06 2019 +0000
@@ -3,8 +3,7 @@
   imports Spec 
 begin
 
-
-section {* The Lexer Functions by Sulzmann and Lu  *}
+section {* The Lexer Functions by Sulzmann and Lu  (without simplification) *}
 
 fun 
   mkeps :: "rexp \<Rightarrow> val"
@@ -274,7 +273,7 @@
 using Posix1(1) lexer_correct_None lexer_correct_Some by blast
 
 
-
+subsection {* A slight reformulation of the lexer algorithm using stacked functions*}
 
 fun flex :: "rexp \<Rightarrow> (val \<Rightarrow> val) => string \<Rightarrow> (val \<Rightarrow> val)"
   where