diff -r 8f89170bb076 -r e0a7ee9842d6 Paper/document/root.tex
--- a/Paper/document/root.tex	Fri Mar 29 01:36:45 2013 +0000
+++ b/Paper/document/root.tex	Fri Mar 29 02:40:38 2013 +0000
@@ -50,16 +50,21 @@
 
 \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 of computation.  We
-formalise Turing machines and relate them to abacus machines and
-recursive functions. We also formalise a universal Turing machine and
-Hoare-style 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 
+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 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
+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.
+%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.}