--- a/Paper/Paper.thy	Thu Mar 07 11:52:08 2013 +0000
+++ b/Paper/Paper.thy	Thu Mar 07 13:19:42 2013 +0000
@@ -720,7 +720,7 @@
   \begin{tabular}[t]{@ {}l@ {}}
   @{thm (lhs) tcopy_begin_def} @{text "\<equiv>"}\\
   \hspace{2mm}@{text "["}@{text "(W\<^bsub>Bk\<^esub>, 0), (R, 2), (R, 3),"}\\
-  \hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W1, 3), (L, 4),"}\\
+  \hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W\<^bsub>Oc\<^esub>, 3), (L, 4),"}\\
   \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} 
   \end{tabular}
   &

Binary file paper.pdf has changed