--- a/Paper.thy	Sun Dec 30 22:15:54 2012 +0000
+++ b/Paper.thy	Thu Jan 03 00:44:20 2013 +0000
@@ -29,20 +29,22 @@
 computable means. The same problem would arise if we had formulated
 the algorithms as recursive functions, because internally in
 Isabelle/HOL, like in all HOL-based theorem provers, functions are
-represented as inductively defined predicates.
+represented as inductively defined predicates too.
 
-The only satisfying way out is to formalise a theory of
-computability. Norrish provided such a formalisation for the HOL4
-theorem prover. He choose the $\lambda$-calculus as the starting point
-for his formalisation, because of its ``simplicity'' \cite[Page
-297]{Norrish11}.  Part of his formalisation is a clever infrastructure
-for reducing $\lambda$-terms. He also established the computational
-equivalence between the lambda-calculus and recursive functions.
-Nevertheless he concluded that it would be appealing to have
-formalisations of more operational models of computations such as
-Turing machines or register machines.  One reason is that many proofs
-in the literature refer to them.  He noted however that in the context
-of theorem provers \cite[Page 310]{Norrish11}:
+The only satisfying way out in a theorem prover based on classical
+logic is to formalise a theory of computability. Norrish provided such
+a formalisation for the HOL4 theorem prover. He choose the
+$\lambda$-calculus as the starting point for his formalisation
+of computability theory,
+because of its ``simplicity'' \cite[Page 297]{Norrish11}.  Part of his
+formalisation is a clever infrastructure for reducing
+$\lambda$-terms. He also established the computational equivalence
+between the $\lambda$-calculus and recursive functions.  Nevertheless he
+concluded that it would be ``appealing'' to have formalisations for more
+operational models of computations, such as Turing machines or register
+machines.  One reason is that many proofs in the literature refer to
+them.  He noted however that in the context of theorem provers
+\cite[Page 310]{Norrish11}:
 
 \begin{quote}
 \it``If register machines are unappealing because of their 
@@ -51,7 +53,16 @@
 \end{quote}
 
 \noindent
-In this paper 
+In this paper we took on this daunting prospect and provide a formalisation
+of Turing machines, as well as Abacus machines (a kind of register machine)
+and recursive functions. Theorem provers are at their best when the data-structures 
+at hand are ``structurally'' defined (like lists, natural numbers,
+regular expressions, etc). The reason why reasoning about Turing machines 
+is challenging is because they are essentially ... 
+
+
+For this we followed mainly the informal
+proof given in the textbook \cite{Boolos87}.
 
 
 
@@ -71,7 +82,7 @@
 section {* Formalisation *}
 
 text {*
-
+  
 *}