--- a/Paper/document/root.tex	Tue Feb 05 12:41:00 2013 +0000
+++ b/Paper/document/root.tex	Wed Feb 06 02:25:00 2013 +0000
@@ -54,7 +54,7 @@
 precludes \emph{direct} reasoning about computability: every boolean
 predicate is either true or false because of the law of excluded
 middle. The only way to reason about computability in a classical
-theorem prover is to formalise a concrete model for computation.  We
+theorem prover is to formalise a concrete model of computation.  We
 formalise Turing machines and relate them to abacus machines and
 recursive functions. We also formalise a universal Turing machine and
 Hoare-style reasoning techniques that allow us to reason about Turing machine