--- a/thys/Paper/Paper.thy	Wed May 11 12:20:16 2016 +0100
+++ b/thys/Paper/Paper.thy	Wed May 11 13:12:30 2016 +0100
@@ -824,7 +824,7 @@
   then record in the calculated value which parts of the string were matched
   by this part. The label can then serve as classification for the tokens.
   For this recall the regular expression @{text "(r\<^bsub>key\<^esub> + r\<^bsub>id\<^esub>)\<^sup>\<star>"} for
-  keywords and identifiers from the Introduction. With record regular
+  keywords and identifiers from the Introduction. With the record regular
   expression we can form \mbox{@{text "((key : r\<^bsub>key\<^esub>) + (id : r\<^bsub>id\<^esub>))\<^sup>\<star>"}}
   and then traverse the calculated value and only collect the underlying
   strings in record values. With this we obtain finite sequences of pairs of
@@ -849,14 +849,14 @@
   While the simplification of regular expressions according to 
   rules like
 
-  \begin{center}
-  \begin{tabular}{lcl}
+  \begin{equation}\label{Simpl}
+  \begin{array}{lcl}
   @{term "ALT ZERO r"} & @{text "\<Rightarrow>"} & @{term r}\\
   @{term "ALT r ZERO"} & @{text "\<Rightarrow>"} & @{term r}\\
   @{term "SEQ ONE r"}  & @{text "\<Rightarrow>"} & @{term r}\\
   @{term "SEQ r ONE"}  & @{text "\<Rightarrow>"} & @{term r}
-  \end{tabular}
-  \end{center}
+  \end{array}
+  \end{equation}
 
   \noindent is well understood, there is an obstacle with the POSIX value
   calculation algorithm by Sulzmann and Lu: if we build a derivative regular
@@ -892,7 +892,8 @@
 
   \noindent
   The functions @{text "simp\<^bsub>Alt\<^esub>"} and @{text "simp\<^bsub>Seq\<^esub>"} encode the simplification rules
-  and compose the rectification functions. The main simplification function is then 
+  in \eqref{Simpl} and compose the rectification functions (simplifications can occur
+  deep inside the regular expression). The main simplification function is then 
 
   \begin{center}
   \begin{tabular}{lcl}
@@ -924,8 +925,8 @@
   and then simplify the result. This gives us a simplified derivative
   @{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, we need to rectify
-  it (that is construct @{term "f\<^sub>r v"}). We can prove that
+  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
 
   \begin{theorem}
   @{thm slexer_correctness}
@@ -1173,7 +1174,8 @@
   \noindent
   {\bf Acknowledgements:}
   We are very grateful to Martin Sulzmann for his comments on our work and 
-  also patiently explaining to us the details in \cite{Sulzmann2014}.
+  moreover patiently explaining to us the details in \cite{Sulzmann2014}. We
+  also received very helpful comments from James Cheney and anonymous referees.
   \small
   \bibliographystyle{plain}
   \bibliography{root}