--- a/Paper/document/root.tex	Mon Apr 01 21:38:53 2013 +0100
+++ b/Paper/document/root.tex	Fri Apr 05 09:18:17 2013 +0100
@@ -62,8 +62,9 @@
 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
-to reason about Turing machine and abacus programs. Our theory can be
-used to formalise other computability results.
+to reason about concrete Turing machine and abacus programs. 
+%Our theory can be
+%used to formalise other computability results.
 %We give one example about the computational equivalence of 
 %single-sided Turing machines. 
 %{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses