--- a/Paper/Paper.thy	Mon Apr 01 21:38:53 2013 +0100
+++ b/Paper/Paper.thy	Fri Apr 05 09:18:17 2013 +0100
@@ -300,9 +300,16 @@
 %represented as inductively defined predicates too.
 
 \noindent
-The motivation of this paper is to bring the ability to reason
-about results from computability theory, for example decidability of the halting problem,
-to the theorem prover Isabelle/HOL.  Norrish formalised computability
+One concete model of computation are Turing machines. We use them 
+in the theorem prover Isabelle/HOL for mechanising  results from 
+computability theory, for example the undecidability of the halting problem.
+Reasoning about decidability is not as straightforward  as one might think
+in Isabelle/HOL and other HOL theorem provers,
+since they are based on classical logic where the law of excluded
+middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always provable no
+matter whether the predicate @{text P} is constructed by computable means.
+
+Norrish formalised computability
 theory in HOL4. 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