changeset 77 | 04e5850818c8 |
parent 76 | 04399b471108 |
child 78 | 2669235c4b1e |
--- 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.