--- a/thys/Paper/Paper.thy	Tue Mar 08 11:40:36 2016 +0000
+++ b/thys/Paper/Paper.thy	Tue Mar 08 12:02:25 2016 +0000
@@ -961,16 +961,16 @@
   ordering (from all possible solutions). The only difference between their
   GREEDY ordering and the ``ordering'' by Sulzmann and Lu is that GREEDY, if
   possible, always prefers a $Left$-value over a $Right$-value, no matter
-  what the underlying string is. This seems like only a very minor
-  difference, but it leads to drastic consequences in terms what
+  what the underlying string is. This seems to be only a very minor
+  difference, but it has drastic consequences in terms of what
   properties both orderings enjoy. What is interesting for our purposes is
   that the properties reflexivity, totality and transitivity for this GREEDY
   ordering can be proved relatively easily by induction.
 
   These properties of GREEDY, however, do not transfer to the POSIX
-  ``ordering'' by Sulzmann and Lu. To start with, $v \geq_r v′$ is not
-  defined inductively, but as $v = v′$ or $v >_r v′ \wedge |v| = |v′|$. This
-  means that $v >_r v′$ does not imply $v \geq_r v′$. Moreover, transitivity
+  ``ordering'' by Sulzmann and Lu. To start with, $v \geq_r v'$ is not
+  defined inductively, but as $v = v'$ or $v >_r v' \wedge |v| = |v'|$. This
+  means that $v >_r v'$ does not imply $v \geq_r v'$. Moreover, transitivity
   does not hold in the ``usual'' formulation, for example:
 
 \begin{proposition}
@@ -979,14 +979,14 @@
 then $v_1 \posix_r v_3$.
 \end{proposition}
 
-\noindent If formulated like this, then there are various counter examples:
-FOr example let $r$ be $a + ((a + a)\cdot (a + \textbf{0}))$ then the $v_1$,
+\noindent If formulated in this way, then there are various counter examples:
+For example let $r$ be $a + ((a + a)\cdot (a + \textbf{0}))$ then the $v_1$,
 $v_2$ and $v_3$ below are values of $r$:
 
 \begin{center}
 \begin{tabular}{lcl}
  $v_1$ & $=$ & $Left(Char\;a)$\\
- $v_2$ & $=$ & $Right((Left(Char\;a), Right(Void)))$\\
+ $v_2$ & $=$ & $Right((Left(Char\;a), Right()))$\\
  $v_3$ & $=$ & $Right((Right(Char\;a), Left(Char\;a)))$
 \end{tabular}
 \end{center}
@@ -994,7 +994,7 @@
 \noindent Moreover $v_1 \posix_r v_2$ and $v_2 \posix_r v_3$,
 but \emph{not} $v_1 \posix_r v_3$! The reason is that although
 $v_3$ is a $Right$-value, it can match a longer string, namely
-$|v_3| = aa$, while $|v_1|$ (and $|v_2|$) matches only $a$. So
+$|v_3| = [a,a]$, while $|v_1|$ (and $|v_2|$) matches only $[a]$. So
 transitivity in this formulation does not hold---in this
 example actually $v_3 \posix_r v_1$!
 
@@ -1003,26 +1003,26 @@
 underlying strings are of the same length. This excludes the
 counter example above and any counter-example we were able 
 to find (by hand and by machine). Thus the transitivity 
-lemma in should be formulated as:
+lemma should be formulated as:
 
-\begin{property}
+\begin{proposition}
 Suppose $v_1 : r$, $v_2 : r$ and 
 $v_3 : r$, and also $|v_1|=|v_2|=|v_3|$.\\
 If $v_1 \posix_r v_2$ and $v_2 \posix_r v_3$
 then $v_1 \posix_r v_3$.
-\end{property}
+\end{proposition}
 
-\noindent While we agree with Sulzmann and Lu that this property probably
+\noindent While we agree with Sulzmann and Lu that this property probably(!)
 holds, proving it seems not so straightforward: although one begins with the
 assumption that the values have the same flattening, this
 cannot be maintained as one descends into the induction. This is 
-a problem that occurs in a number of places in their proof.
-Sulzmann and Lu do not give an explicit proof
-of the transitivity property, but give a closely related
+a problem that occurs in a number of places in the proofs by Sulzmann and Lu.
+
+Although they do not give an explicit proof
+of the transitivity property, they give a closely related
 property about the existence of maximal elements. They state
 that this can be verified by an induction on $r$. We disagree
 with this as we shall show next in case of transitivity.
-
 The case where the reasoning breaks down is the sequence case,
 say $r_1\cdot r_2$. The induction hypotheses in this case
 are
@@ -1067,9 +1067,9 @@
 namely:
 
 \begin{equation}
-|(v_{1l}, v_{1r})| = |(v_{2l}, v_{2r})|
+|Seq\,v_{1l}\, v_{1r}| = |Seq\,v_{2l}\, v_{2r}|
 \qquad\textrm{and}\qquad
-|(v_{2l}, v_{2r})| = |(v_{3l}, v_{3r})|
+|Seq\,v_{2l}\, v_{2r}| = |Seq\,v_{3l}\, v_{3r}|
 \label{lens}
 \end{equation}
 
@@ -1077,7 +1077,7 @@
 We need to show that
 
 \[
-Seq\,v_{1l}\, v_{1r}) \posix_{r_1\cdot r_2} Seq\, v_{3l}\, v_{3r}
+Seq\,v_{1l}\, v_{1r} \posix_{r_1\cdot r_2} Seq\, v_{3l}\, v_{3r}
 \]
 
 \noindent holds. We can proceed by analysing how the
@@ -1109,7 +1109,7 @@
 \noindent but still \eqref{lens} will hold. Now we are stuck,
 since the IH does not apply. As said, this problem where the
 induction hypothesis does not apply arises in several places in
-the proof of Sulzmann and LU, not just when proving transitivity.
+the proof of Sulzmann and Lu, not just for proving transitivity.
 
 *}