--- a/thys/Paper/Paper.thy	Mon May 16 12:50:37 2016 +0100
+++ b/thys/Paper/Paper.thy	Mon May 16 15:20:23 2016 +0100
@@ -927,7 +927,19 @@
   @{text "r\<^sub>s"} and a rectification function @{text "f\<^sub>r"}. The lexer
   is then recursively called with the simplified derivative, but before
   we inject the character @{term c} into the value @{term v}, we need to rectify
-  @{term v} (that is construct @{term "f\<^sub>r v"}). We can prove that
+  @{term v} (that is construct @{term "f\<^sub>r v"}). Before we can establish the correctness
+  of @{const "slexer"}, we need to show that simplification preserves the language
+  and the relation between simplification and our posix definition:
+
+  \begin{lemma}\mbox{}\smallskip\\
+  \begin{tabular}{ll}
+  (1) & @{thm L_fst_simp[symmetric]}\\
+  (2) & @{thm[mode=IfThen] Posix_simp}
+  \end{tabular}
+  \end{lemma}
+
+  \noindent
+  We can now prove that
 
   \begin{theorem}
   @{thm slexer_correctness}