diff -r 44fec0bfffe5 -r ac831326441c thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Tue Mar 08 07:17:31 2016 +0000
+++ b/thys/Paper/Paper.thy	Tue Mar 08 07:19:55 2016 +0000
@@ -1036,9 +1036,9 @@
 We can assume that 
 
 \begin{equation}
-(v_{1l}, v_{1r}) \posix^{r_1\,r_2} (v_{2l}, v_{2r})
+Seq\,v_{1l}\, v_{1r}) \posix_{r_1\,r_2} Seq\,v_{2l}\, v_{2r})
 \qquad\textrm{and}\qquad
-(v_{2l}, v_{2r}) \posix^{r_1\,r_2} (v_{3l}, v_{3r})
+Seq\,v_{2l}\, v_{2r}) \posix_{r_1\,r_2} Seq\,v_{3l}\, v_{3r})
 \label{assms}
 \end{equation}
 
@@ -1057,7 +1057,7 @@
 We need to show that
 
 \[
-(v_{1l}, v_{1r}) \posix^{r_1\,r_2} (v_{3l}, v_{3r})
+(v_{1l}, v_{1r}) \posix_{r_1\,r_2} (v_{3l}, v_{3r})
 \]
 
 \noindent holds. We can proceed by analysing how the
@@ -1066,9 +1066,9 @@
 we know 
 
 \[
-v_{1l} \posix^{r_1} v_{2l}
+v_{1l} \posix_{r_1} v_{2l}
 \qquad\textrm{and}\qquad
-v_{2l} \posix^{r_1} v_{3l}
+v_{2l} \posix_{r_1} v_{3l}
 \]
 
 \noindent and also know the corresponding typing judgements.
@@ -1087,9 +1087,7 @@
 \]
 
 \noindent but still \eqref{lens} will hold. Now we are stuck,
-since the IH does not apply. Sulzmann and Lu overlook this
-fact and just apply the IHs. Obviously nothing which a 
-theorem prover allows us to do.
+since the IH does not apply. 
 
 
 *}