author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
Thu, 24 Jan 2013 17:15:42 +0100 | |
changeset 77 | 04e5850818c8 |
parent 76 | 04399b471108 |
child 78 | 2669235c4b1e |
Paper/Paper.thy | file | annotate | diff | comparison | revisions | |
paper.pdf | file | annotate | diff | comparison | revisions |
--- a/Paper/Paper.thy Thu Jan 24 17:14:39 2013 +0100 +++ b/Paper/Paper.thy Thu Jan 24 17:15:42 2013 +0100 @@ -583,7 +583,7 @@ \end{tabular} \end{center} - \noindet + \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.