--- 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.