diff -r 2669235c4b1e -r bc54c5e648d7 Paper/document/root.tex --- a/Paper/document/root.tex Thu Jan 24 17:40:04 2013 +0100 +++ b/Paper/document/root.tex Thu Jan 24 18:59:49 2013 +0100 @@ -53,7 +53,7 @@ theorem prover is to formalise a concrete model for computation. We formalise Turing machines and relate them to abacus machines and recursive functions. We also formalise a universal Turing machine and -reasoning techniques that allow us to reason about Turing machine +Hoare-style reasoning techniques that allow us to reason about Turing machine programs. Our theory can be used to formalise other computability results. We give one example about the computational equivalence of single-sided Turing machines.