--- 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 "]"} 

Binary file paper.pdf has changed

--- a/thys/uncomputable.thy	Sun Jan 27 17:15:38 2013 +0000
+++ b/thys/uncomputable.thy	Sun Jan 27 20:01:13 2013 +0000
@@ -49,7 +49,7 @@
                 (R, 2), (R, 2), (L, 5), (W0, 4),
                 (R, 0), (L, 5)]"
 
-idefinition 
+definition 
   tcopy :: "instr list"
 where
   "tcopy \<equiv> (tcopy_begin |+| tcopy_loop) |+| tcopy_end"
@@ -137,7 +137,7 @@
 
 lemma init_halt: 
   "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (Suc 0, [], Oc\<up>x) tcopy_begin stp)"
-proof(rule_tac LE = init_LE in halt_lemma)
+proof(rule_tac LE = init_LE in halt_lemma) 
   show "wf init_LE" by(simp add: wf_begin_le)
 next
   assume h: "0 < x"