--- a/document/root.tex	Sun Jan 13 23:59:29 2013 +0000
+++ b/document/root.tex	Mon Jan 14 21:40:38 2013 +0000
@@ -1,4 +1,5 @@
-\documentclass[10pt, conference, compsocconf]{IEEEtran}
+\documentclass[runningheads]{llncs}
+%\documentclass[10pt, conference, compsocconf]{IEEEtran}
 \usepackage{isabelle}
 \usepackage{isabellesym}
 \usepackage{times}
@@ -25,16 +26,10 @@
 \newcommand{\isasymurcorner}{$\urcorner$}
 \begin{document}
 
+
 \title{Formalising Computability Theory in Isabelle/HOL}
-
-
-\author{
-\IEEEauthorblockN{Jian Xu, Xingyuan Zhang}
-\IEEEauthorblockA{PLA University of Science and Technology Nanjing, China}
-\and
-\IEEEauthorblockN{Christian Urban}
-\IEEEauthorblockA{King's College London, UK}
-}
+\author{Jian Xu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}}
+\institute{PLA University of Science and Technology, China \and King's College London, UK}
 
 \maketitle
 
@@ -52,13 +47,6 @@
 the notion of a universal Turing machine.
 \end{abstract}
 
-\begin{IEEEkeywords}
-Turing Machines, Computability, Isabelle/HOL, Wang tilings
-\end{IEEEkeywords}
-
-
-\IEEEpeerreviewmaketitle
-
 % generated text of all theories
 \input{session}