--- a/thys/Paper/Paper.thy	Tue Mar 08 11:34:51 2016 +0000
+++ b/thys/Paper/Paper.thy	Tue Mar 08 11:40:36 2016 +0000
@@ -946,17 +946,17 @@
 \end{center}
 
   \noindent
-  The idea behind the rules $(A1)$ and $(A2)$ is that a $Left$-value is
+  The idea behind the rules $(A1)$ and $(A2)$, for example, is that a $Left$-value is
   bigger than a $Right$-value, if the underlying string of the $Left$-value is
-  bigger or equals to the underlying string of the $Right$-value. The order
-  is reversed if the $Right$-value can match longer string than a $Left$-value.
+  longer or of equal length to the underlying string of the $Right$-value. The order
+  is reversed, however, if the $Right$-value can match longer string than a $Left$-value.
   In this way the POSIX value is supposed to be the biggest value
   for a given string and regular expression.
 
   Sulzmann and Lu explicitly refer to the paper \cite{Frisch2004} by Frisch
   and Cardelli from where they have taken the idea for their correctness
-  proof of the POSIX value algorithm. Frisch and Cardelli introduced a
-  similar ordering for GREEDY matching and they show that their greedy
+  proof. Frisch and Cardelli introduced a
+  similar ordering for GREEDY matching and they show that their GREEDY
   matching algorithm always produces a maximal element according to this
   ordering (from all possible solutions). The only difference between their
   GREEDY ordering and the ``ordering'' by Sulzmann and Lu is that GREEDY, if