--- a/thys/Paper/Paper.thy	Tue May 17 11:16:56 2016 +0100
+++ b/thys/Paper/Paper.thy	Tue May 17 14:28:22 2016 +0100
@@ -879,9 +879,9 @@
   @{thm (lhs) F_SEQ1.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 ()) (f\<^sub>2 v)"}\\
   @{thm (lhs) F_SEQ2.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 v) (f\<^sub>2 ())"}\\
   @{thm (lhs) F_SEQ.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)"}\medskip\\
-  \end{tabular}
-
-  \begin{tabular}{lcl}
+  %\end{tabular}
+  %
+  %\begin{tabular}{lcl}
   @{term "simp_ALT (ZERO, DUMMY) (r\<^sub>2, f\<^sub>2)"} & $\dn$ & @{term "(r\<^sub>2, F_RIGHT f\<^sub>2)"}\\
   @{term "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, DUMMY)"} & $\dn$ & @{term "(r\<^sub>1, F_LEFT f\<^sub>1)"}\\
   @{term "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2)"} & $\dn$ & @{term "(ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)"}\\
@@ -904,10 +904,10 @@
   \end{tabular}
   \end{center} 
 
-  \noindent where @{term "id"} stands for the identity function. This
-  function returns a simplified regular expression and a corresponding
+  \noindent where @{term "id"} stands for the identity function. The
+  function @{const simp} returns a simplified regular expression and a corresponding
   rectification function. Note that we do not simplify under stars: this
-  seems to slow down the algorithm, rather than speed up. The optimised
+  seems to slow down the algorithm, rather than speed it up. The optimised
   lexer is then given by the clauses:
   
   \begin{center}
@@ -945,7 +945,7 @@
   r\<^sub>2"} cases. In each case we have to analyse four subcases whether
   @{term "fst (simp r\<^sub>1)"} and @{term "fst (simp r\<^sub>2)"} equals @{const
   ZERO} (respectively @{const ONE}). For example for @{term "r = ALT
-  r\<^sub>1 r\<^sub>2"}, considder the subcase @{term "fst (simp r\<^sub>1) = ZERO"} and
+  r\<^sub>1 r\<^sub>2"}, consider the subcase @{term "fst (simp r\<^sub>1) = ZERO"} and
   @{term "fst (simp r\<^sub>2) \<noteq> ZERO"}. By assumption we know @{term "s \<in>
   fst (simp (ALT r\<^sub>1 r\<^sub>2)) \<rightarrow> v"}. From this we can infer @{term "s \<in> fst (simp r\<^sub>2) \<rightarrow> v"}
   and by IH also (*) @{term "s \<in> r\<^sub>2 \<rightarrow> (snd (simp r\<^sub>2) v)"}. Given @{term "fst (simp r\<^sub>1) = ZERO"}
@@ -1052,7 +1052,8 @@
   relatively easily by induction.
 
   These properties of GREEDY, however, do not transfer to the POSIX
-  ``ordering'' by Sulzmann and Lu. To start with, @{text "v\<^sub>1 \<ge>r v\<^sub>2"} is
+  ``ordering'' by Sulzmann and Lu, which they define as @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"}. 
+  To start with, @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"} is
   not defined inductively, but as @{term "v\<^sub>1 = v\<^sub>2"} or @{term "(v\<^sub>1 >r
   v\<^sub>2) \<and> (flat v\<^sub>1 = flat (v\<^sub>2::val))"}. This means that @{term "v\<^sub>1
   >(r::rexp) (v\<^sub>2::val)"} does not necessarily imply @{term "v\<^sub>1 \<ge>(r::rexp)