# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1365149897 -3600
# Node ID 6b6d71d14e7575add5e8c62f8fae037f55cce838
# Parent  0b9c893cfd1ba630b3257aa71f15db5e30e4200b
polished the intro

diff -r 0b9c893cfd1b -r 6b6d71d14e75 Paper/Paper.thy
--- 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
diff -r 0b9c893cfd1b -r 6b6d71d14e75 Paper/document/root.tex
--- a/Paper/document/root.tex	Mon Apr 01 21:38:53 2013 +0100
+++ b/Paper/document/root.tex	Fri Apr 05 09:18:17 2013 +0100
@@ -62,8 +62,9 @@
 universal function and obtaining from it a universal Turing machine by
 our verified translation from recursive functions to abacus programs
 and from abacus programs to Turing machine programs.  Hoare-style reasoning techniques allow us
-to reason about Turing machine and abacus programs. Our theory can be
-used to formalise other computability results.
+to reason about concrete Turing machine and abacus programs. 
+%Our theory can be
+%used to formalise other computability results.
 %We give one example about the computational equivalence of 
 %single-sided Turing machines. 
 %{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses
diff -r 0b9c893cfd1b -r 6b6d71d14e75 paper.pdf
Binary file paper.pdf has changed