--- a/Paper.thy	Thu Jan 03 00:53:14 2013 +0000
+++ b/Paper.thy	Fri Jan 04 13:10:30 2013 +0000
@@ -31,7 +31,7 @@
 Isabelle/HOL, like in all HOL-based theorem provers, functions are
 represented as inductively defined predicates too.
 
-The only satisfying way out in a theorem prover based on classical
+The only satisfying way out of this problem 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
@@ -42,7 +42,7 @@
 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
+machines.  One reason is that many proofs in the literature use 
 them.  He noted however that in the context of theorem provers
 \cite[Page 310]{Norrish11}:
 
@@ -55,9 +55,24 @@
 \noindent
 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 
+and recursive functions. To see the difficulties involved with this work one
+has to understantd that interactive theorem provers, like Isabelle/HOL, 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 
+regular expressions, etc). For them, they come with a convenient reasoning 
+infrastructure (for example induction principles, recursion combinators and so on).
+But this is not the case with Turing machines  (and also register machines): 
+underlying their definition is a set of states
+together with a transition function, both of which are not structurally defined. 
+This means we have to implement our own reasoning infrastructure. This often
+leads to annoyingly lengthy and detailed formalisations.  We noticed first 
+the difference between both ``worlds'' when formalising the Myhill-Nerode 
+theorem ??? where regular expressions fared much better than automata. 
+However, with Turing machines there seems to be no alternative, because they
+feature frequently in proofs. We will analyse one case, Wang tilings, at the end 
+of the paper, which uses also the notion of a Universal Turing Machine.
+
+The reason why reasoning about Turing machines 
 is challenging is because they are essentially ...