# HG changeset patch # User Christian Urban <christian dot urban at kcl dot ac dot uk> # Date 1359045604 -3600 # Node ID 2669235c4b1ec3d9f5008f1a68017d80abd8c22d # Parent 04e5850818c89ebdb9aeddf1f2d4c18813706907 updated paper diff -r 04e5850818c8 -r 2669235c4b1e Paper/Paper.thy --- a/Paper/Paper.thy Thu Jan 24 17:15:42 2013 +0100 +++ b/Paper/Paper.thy Thu Jan 24 17:40:04 2013 +0100 @@ -550,7 +550,7 @@ \begin{center} \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} \begin{tabular}[t]{@ {}l@ {}} - @{thm (lhs) Hoare_halt_def} @{text "\<equiv>"}\\ + @{thm (lhs) Hoare_halt_def} @{text "\<equiv>"}\\[1mm] \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\ \hspace{7mm}if @{term "P (l, r)"} holds then\\ \hspace{7mm}@{text "\<exists>"} @{term n}. such that\\ @@ -558,7 +558,7 @@ \hspace{7mm}@{text "Q holds_for (steps (1, (l, r)) p n)"} \end{tabular} & \begin{tabular}[t]{@ {}l@ {}} - @{thm (lhs) Hoare_unhalt_def} @{text "\<equiv>"}\\ + @{thm (lhs) Hoare_unhalt_def} @{text "\<equiv>"}\\[1mm] \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\ \hspace{7mm}if @{term "P (l, r)"} holds then\\ \hspace{7mm}@{text "\<forall>"} @{term n}. @{text "\<not> is_final (steps (1, (l, r)) p n)"} @@ -586,7 +586,7 @@ \noindent {\it unfold} The first states that on a tape @{term "(Bk \<up> n, [Oc, Oc])"} halts in tree steps leaving the tape unchanged. In the other states - that @{term dither} started with tape @{term "(Bk \<up> n, [Oc, Oc])"} loops. + that @{term dither} started with tape @{term "(Bk \<up> n, [Oc])"} loops. diff -r 04e5850818c8 -r 2669235c4b1e paper.pdf Binary file paper.pdf has changed