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