--- a/document/root.tex	Thu Jan 10 01:46:51 2013 +0000
+++ b/document/root.tex	Thu Jan 10 07:20:28 2013 +0000
@@ -45,7 +45,7 @@
 prover is to formalise a concrete model for computation. 
 We formalise Turing machines and relate them to abacus machines and recursive
 functions. Our theory can be used to formalise other computability results:
-we give one example about the undecidability of Wang tilings, whose proof uses
+we give one example about the undecidability of Wang's tiling problem, whose proof uses
 the notion of a universal Turing machine.
 \end{abstract}