# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1359316873 0
# Node ID b9d0dd18c81e5a0cee478a5424f60a5feba834b6
# Parent  2068654bdf54ae2da3992265c915257218464aeb
updated paper

diff -r 2068654bdf54 -r b9d0dd18c81e Paper/Paper.thy
--- 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 "]"} 
diff -r 2068654bdf54 -r b9d0dd18c81e paper.pdf
Binary file paper.pdf has changed
diff -r 2068654bdf54 -r b9d0dd18c81e thys/uncomputable.thy
--- 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"