diff -r c8ff97d9f8da -r 7edbd5657702 Paper/Paper.thy
--- a/Paper/Paper.thy	Sun Jan 20 16:01:16 2013 +0000
+++ b/Paper/Paper.thy	Tue Jan 22 14:38:56 2013 +0000
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../thys/uncomputable"
+imports "../thys/recursive"
 begin
 
 (*
@@ -66,7 +66,7 @@
 
 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. He choose
+provided such a formalisation for the HOL. 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
@@ -90,13 +90,13 @@
 of register machines) and recursive functions. To see the difficulties
 involved with this work, one has to understand that Turing machine
 programs can be completely \emph{unstructured}, behaving 
-similar to Basic's infamous goto \cite{Dijkstra68}. This precludes in the
+similar Basic programs involving the infamous goto \cite{Dijkstra68}. This precludes in the
 general case a compositional Hoare-style reasoning about Turing
-programs.  We provide such Hoare-rules for when it is possible to
+programs.  We provide such Hoare-rules for when it \emph{is} possible to
 reason in a compositional manner (which is fortunately quite often), but also tackle 
 the more complicated case when we translate abacus programs into 
-Turing programs.  This aspect of reasoning about computability theory 
-is usually completely left out in the informal literature, e.g.~\cite{Boolos87}.
+Turing programs.  These difficulties when reasoning about computability theory 
+are usually completely left out in the informal literature, e.g.~\cite{Boolos87}.
 
 %To see the difficulties
 %involved with this work, one has to understand that interactive