--- a/Paper/Paper.thy	Sun Jan 27 17:15:38 2013 +0000
+++ b/Paper/Paper.thy	Sun Jan 27 20:01:13 2013 +0000
@@ -22,7 +22,7 @@
   update2 ("update") and
   tm_wf0 ("wf") and
   (*is_even ("iseven") and*)
-  tcopy_init ("copy\<^bsub>begin\<^esub>") and
+  tcopy_begin ("copy\<^bsub>begin\<^esub>") and
   tcopy_loop ("copy\<^bsub>loop\<^esub>") and
   tcopy_end ("copy\<^bsub>end\<^esub>") and
   step0 ("step") and
@@ -529,7 +529,7 @@
   \begin{center}
   \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c}
   \begin{tabular}[t]{@ {}l@ {}}
-  @{thm (lhs) tcopy_init_def} @{text "\<equiv>"}\\
+  @{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 "(L, 4), (L, 0)"}@{text "]"}