--- a/Journal/document/root.tex	Thu Jun 02 16:44:35 2011 +0000
+++ b/Journal/document/root.tex	Thu Jun 02 20:02:16 2011 +0000
@@ -1,4 +1,4 @@
-\documentclass[runningheads]{llncs}
+\documentclass{ita}
 \usepackage{isabelle}
 \usepackage{isabellesym}
 \usepackage{amsmath}
@@ -16,8 +16,6 @@
 %%\usepackage{mathabx}
 \usepackage{stmaryrd}
 
-\titlerunning{Myhill-Nerode using Regular Expressions}
-
 
 \urlstyle{rm}
 \isabellestyle{it}
@@ -36,13 +34,13 @@
 \newcommand{\bigplus}{\mbox{\Large\bf$+$}}
 \begin{document}
 
-\title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular
-  Expressions (Proof Pearl)}
-\author{Chunhan Wu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}}
-\institute{PLA University of Science and Technology, China \and TU Munich, Germany}
-\maketitle
+\title{A Formalisation of the Myhill-Nerode Theorem based on Regular
+  Expressions}
+\author{Chunhan Wu}\address{PLA University of Science and Technology, China}
+\author{Xingyuan Zhang}\sameaddress{1}
+\author{Christian Urban}\address{TU Munich,
+  Germany}\secondaddress{corresponding author}
 
-%\mbox{}\\[-10mm]
 \begin{abstract} 
 There are numerous textbooks on regular languages. Nearly all of them
 introduce the subject by describing finite automata and only mentioning on the
@@ -55,9 +53,8 @@
 reasoning infrastructure comes for free. We show in this paper that a central
 result from formal language theory---the Myhill-Nerode theorem---can be
 recreated using only regular expressions.
-
 \end{abstract}
-
+\maketitle
 
 \input{session}