diff -r 6d89ed67ba27 -r 00ae320bb804 document/root.tex --- 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}