--- a/Paper/Paper.thy	Fri Jan 18 23:59:33 2013 +0000
+++ b/Paper/Paper.thy	Sat Jan 19 12:45:14 2013 +0000
@@ -72,7 +72,7 @@
 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''
+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 use them.  He noted
@@ -232,7 +232,7 @@
   Note that by using lists each side of the tape is only finite. The
   potential infinity is achieved by adding an appropriate blank or occupied cell 
   whenever the head goes over the ``edge'' of the tape. To 
-  make this formal we define five possible \emph{actions} 
+  make this formal we define five possible \emph{actions}, @{text a} 
   the Turing machine can perform:
 
   \begin{center}