diff -r 21c980a85ee5 -r 44fec0bfffe5 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Tue Mar 08 07:14:52 2016 +0000
+++ b/thys/Paper/Paper.thy	Tue Mar 08 07:17:31 2016 +0000
@@ -1012,22 +1012,22 @@
 \begin{tabular}{@ {}ll@ {}}
 IH $r_1$:\\
 $\forall v_1, v_2, v_3.$ 
-  & $\vdash v_1 : r_1\;\wedge$\\
-  & $\vdash v_2 : r_1\;\wedge$\\
-  & $\vdash v_3 : r_1\;\wedge$\\
+  & $v_1 : r_1\;\wedge$\\
+  & $v_2 : r_1\;\wedge$\\
+  & $v_3 : r_1\;\wedge$\\
   & $|v_1|=|v_2|=|v_3|\;\wedge$\\
-  & $v_1 \posix^{r_1} v_2\;\wedge\; v_2 \posix^{r_1} v_3$\medskip\\
-  & $\;\;\Rightarrow v_1 \posix^{r_1} v_3$
+  & $v_1 \posix_{r_1} v_2\;\wedge\; v_2 \posix_{r_1} v_3$\medskip\\
+  & $\;\;\Rightarrow v_1 \posix_{r_1} v_3$
 \end{tabular} &
 \begin{tabular}{@ {}ll@ {}}
 IH $r_2$:\\
 $\forall v_1, v_2, v_3.$ 
-  & $\vdash v_1 : r_2\;\wedge$\\
-  & $\vdash v_2 : r_2\;\wedge$\\
-  & $\vdash v_3 : r_2\;\wedge$\\
+  & $v_1 : r_2\;\wedge$\\
+  & $v_2 : r_2\;\wedge$\\
+  & $v_3 : r_2\;\wedge$\\
   & $|v_1|=|v_2|=|v_3|\;\wedge$\\
-  & $v_1 \posix^{r_2} v_2\;\wedge\; v_2 \posix^{r_2} v_3$\medskip\\
-  & $\;\;\Rightarrow v_1 \posix^{r_2} v_3$
+  & $v_1 \posix_{r_2} v_2\;\wedge\; v_2 \posix_{r_2} v_3$\medskip\\
+  & $\;\;\Rightarrow v_1 \posix_{r_2} v_3$
 \end{tabular}
 \end{tabular}
 \end{center}