--- a/Paper/document/root.tex	Sat Jul 27 08:23:09 2013 +0200
+++ b/Paper/document/root.tex	Tue Sep 03 15:02:52 2013 +0100
@@ -58,7 +58,7 @@
 %theorem prover is to formalise a concrete model of computation.  
 Following the textbook by Boolos et al, we formalise Turing machines
 and relate them to abacus machines and recursive functions. We ``tie
-the know'' between these three computational models by formalising a
+the knot'' between these three computational models by formalising a
 universal function and obtaining from it a universal Turing machine by
 our verified translation from recursive functions to abacus programs
 and from abacus programs to Turing machine programs.  Hoare-style reasoning techniques allow us