--- a/thys/Paper/Paper.thy	Tue Mar 08 07:19:55 2016 +0000
+++ b/thys/Paper/Paper.thy	Tue Mar 08 09:25:17 2016 +0000
@@ -903,15 +903,16 @@
   \cite{Sulzmann2014} to be ``rigorous''. Since these are evidently not in
   final form, we make no comment thereon, preferring to give general reasons
   for our belief that the approach of \cite{Sulzmann2014} is problematic.
-  Their central definition is an ``ordering relation''
+  Their central definition is an ``ordering relation'' defined by the
+  rules (slightly adapted to fit our notation):
 
 \begin{center}  
-\begin{tabular}{c@ {\hspace{5mm}}c}		 
+\begin{tabular}{@ {}c@ {\hspace{2mm}}c@ {}}		 
 $\infer{v_{1} \posix_{r_{1}} v'_{1}} 
        {Seq\,v_{1}\,v_{2} \posix_{r_{1}r_{2}} Seq\,v'_{1}\,v'_{2}}(C2)$
 &
 $\infer{v_{2} \posix_{r_{2}} v'_{2}} 
-       {Seq\,v_{1}\,v_{2}) \posix_{r_{1}r_{2}} Seq\,v_{1}\,v'_{2}}(C1)$
+       {Seq\,v_{1}\,v_{2} \posix_{r_{1}r_{2}} Seq\,v_{1}\,v'_{2}}(C1)$
 \medskip\\
 		
 		
@@ -929,14 +930,14 @@
        {Left \; v_{1} \posix_{r_{1}+r_{2}} Left \; v'_{1}}(A4)$ 
 \medskip\\
 
- $\infer{|v :: vs| = []} {[] \posix_{r^{\star}} v :: vs}(K1)$ & 
- $\infer{|v :: vs| \neq []} { v :: vs \posix_{r^{\star}} []}(K2)$
+ $\infer{|v :: vs| = []} {Stars\,[] \posix_{r^{\star}} Stars\,(v :: vs)}(K1)$ & 
+ $\infer{|v :: vs| \neq []} {Stars\,(v :: vs) \posix_{r^{\star}} Stars\,[]}(K2)$
 \medskip\\
 	
 $\infer{ v_{1} \posix_{r} v_{2}} 
-       {v_{1} :: vs_{1} \posix_{r^{\star}} v_{2} :: vs_{2}}(K3)$ & 
-$\infer{ vs_{1} \posix_{r^{\star}} vs_{2}} 
-       {v :: vs_{1} \posix_{r^{\star}} v :: vs_{2}}(K4)$	
+       {Stars\,(v_{1} :: vs_{1}) \posix_{r^{\star}} Stars\,(v_{2} :: vs_{2})}(K3)$ & 
+$\infer{ Stars\,vs_{1} \posix_{r^{\star}} Stars\,vs_{2}} 
+       {Stars\,(v :: vs_{1}) \posix_{r^{\star}} Stars\,(v :: vs_{2})}(K4)$	
 \end{tabular}
 \end{center}
 

Binary file thys/paper.pdf has changed