--- a/document/root.tex	Wed Dec 26 14:52:14 2012 +0000
+++ b/document/root.tex	Wed Dec 26 19:03:06 2012 +0000
@@ -34,28 +34,29 @@
 
 \begin{document}
 
-\title{A Formalised Theorey about Turing Machines in Isablle/HOL}
+\title{A Formalised Theory of Turing Machines in Isabelle/HOL}
 
 
-\author{\IEEEauthorblockN{Authors Name/s per 1st Affiliation (Author)}
-\IEEEauthorblockA{line 1 (of Affiliation): dept. name of organization\\
-line 2: name of organization, acronyms acceptable\\
-line 3: City, Country\\
-line 4: Email: name@xyz.com}
+\author{
+\IEEEauthorblockN{Xu Jian, Xingyuan Zhang}
+\IEEEauthorblockA{PLA University of Science and Technology Nanjing, China}
 \and
-\IEEEauthorblockN{Authors Name/s per 2nd Affiliation (Author)}
-\IEEEauthorblockA{line 1 (of Affiliation): dept. name of organization\\
-line 2: name of organization, acronyms acceptable\\
-line 3: City, Country\\
-line 4: Email: name@xyz.com}
+\IEEEauthorblockN{Christian Urban}
+\IEEEauthorblockA{King's College London, UK}
 }
 
 \maketitle
 
 
 \begin{abstract}
-
-The abstract goes here. DO NOT USE SPECIAL CHARACTERS, SYMBOLS, OR MATH IN YOUR TITLE OR ABSTRACT.
+Isabelle/HOL is an interactive theorem prover based on classical 
+logic. While classical reasoning allow users to take convenient 
+shortcuts in some proofs, it precludes \emph{direct} reasoning about 
+decidability: every boolean predicate is either true or false
+because of the law of excluded middle. The only way to reason
+about decidability in a classical theorem prover, like Isabelle/HOL,
+is to formalise a concrete model for computation. In this paper
+we formalise Turing machines and relate them to register machines.
 
 \end{abstract}
 
@@ -73,16 +74,6 @@
 \parindent 0pt\parskip 0.5ex
 
 
-\section{Introduction}
-
-text {*
-  
-
-*}
-
-
-\noindent
-{\bf Contributions:} 
 
 
 % generated text of all theories