diff -r ba789a0768a2 -r 4ef4b25e2997 Paper.thy --- a/Paper.thy Fri Jan 11 05:45:40 2013 +0000 +++ b/Paper.thy Fri Jan 11 05:49:25 2013 +0000 @@ -150,7 +150,7 @@ formalisation we need arbitrary functions. But the general ideas for how to do this are clear enough in \cite{Boolos87}. However, one aspect that is completely left out from the informal description in -\cite{Boolos87}, and similar ones we are aware of, are arguments why certain Turing +\cite{Boolos87}, and similar ones we are aware of, is arguments why certain Turing machines are correct. We will introduce Hoare-style proof rules which help us with such correctness arguments of Turing machines.