--- a/document/root.tex	Sun Jan 06 23:50:24 2013 +0000
+++ b/document/root.tex	Tue Jan 08 01:21:02 2013 +0000
@@ -16,7 +16,7 @@
 
 \begin{document}
 
-\title{A Formalised Theory of Turing Machines in Isabelle/HOL}
+\title{Formalising Computability Theory in Isabelle/HOL}
 
 
 \author{
@@ -31,19 +31,20 @@
 
 
 \begin{abstract}
-Isabelle/HOL is an interactive theorem prover based on classical 
-logic. While classical reasoning allow users to take convenient 
-shortcuts in some proofs, it precludes \emph{direct} reasoning about 
-decidability: every boolean predicate is either true or false
-because of the law of excluded middle. The only way to reason
-about decidability in a classical theorem prover, like Isabelle/HOL,
-is to formalise a concrete model for computation. In this paper
-we formalise Turing machines and relate them to register machines.
-
+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:
+we give one example about the undecidability of Wang tilings, whose proof uses
+the notion of a universal Turing machine.
 \end{abstract}
 
 \begin{IEEEkeywords}
-Turing Machines, Decidability, Isabelle/HOL;
+Turing Machines, Computability, Isabelle/HOL, Wang tilings
 \end{IEEEkeywords}