# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1457421451 0
# Node ID 44fec0bfffe505bf36915c7d48322531df03699b
# Parent  21c980a85ee5c9a12bb1ecd4fe73e85e7c170978
updated

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} 
diff -r 21c980a85ee5 -r 44fec0bfffe5 thys/paper.pdf
Binary file thys/paper.pdf has changed