--- a/Paper/document/root.tex	Wed Jan 23 20:18:40 2013 +0100
+++ b/Paper/document/root.tex	Thu Jan 24 00:20:26 2013 +0100
@@ -37,7 +37,7 @@
 \begin{document}
 
 
-\title{Mechanising Computability Theory in Isabelle/HOL}
+\title{Mechanising Turing Machines and Computability Theory in Isabelle/HOL}
 \author{Jian Xu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}}
 \institute{PLA University of Science and Technology, China \and King's College London, UK}
 
@@ -45,16 +45,20 @@
 
 
 \begin{abstract}
-We present a formalised theory of computability in the 
-theorem prover Isabelle/HOL. This theorem prover is based on classical 
-logic which 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 formalise Turing machines and relate them to abacus machines and recursive
-functions. Our theory can be used to formalise other computability results:
-{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses
-the notion of a universal Turing machine.}
+We present a formalised theory of computability in the theorem prover
+Isabelle/HOL. This theorem prover is based on classical logic which
+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
+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
+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
+%the notion of a universal Turing machine.}
 \end{abstract}
 
 % generated text of all theories