--- a/Journal/document/root.tex	Wed Dec 12 11:45:04 2012 +0000
+++ b/Journal/document/root.tex	Fri Mar 01 17:13:32 2013 +0000
@@ -1,4 +1,5 @@
-\documentclass[acmtocl,final]{acmtrans2m}
+\documentclass[final, natbib]{svjour3} 
+%\documentclass[acmtocl,final]{acmtrans2m}
 \usepackage{isabelle}
 \usepackage{isabellesym}
 \usepackage{amsmath}
@@ -9,12 +10,17 @@
 \usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
 \usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
 \usetikzlibrary{matrix}
-%%%\usepackage{pdfsetup}
+\usepackage{pdfsetup}
 \usepackage{ot1patch}
 \usepackage{times}
 \usepackage{stmaryrd}
 \usepackage{mathpartir}
 \usepackage{longtable}
+%%\usepackage{chicago}
+
+\def\citeN{\citet}
+
+%%\journalname{Journal of Automated Reasoning}
 
 \urlstyle{rm}
 \isabellestyle{it}
@@ -40,16 +46,24 @@
 \newtheorem{dfntn}{Definition}[section]
 \newtheorem{prpstn}{Proposition}[section]
 
+\begin{document}
 
 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular
-  Expressions$^\star$}
-%%\thanks{This is a revised and expanded version of \cite{WuZhangUrban11}.}
-\author{Chunhan Wu\\PLA University of Science and Technology Nanjing, China \and
-Xingyuan Zhang\\PLA University of Science and Technology Nanjing, China \and
-Christian Urban\\ King's College London, United Kingdom}
+  Expressions$^\star$\thanks{$^\star$ This is a revised and much expanded version of \cite{WuZhangUrban11}.}}
+%\author{Chunhan Wu\\PLA University of Science and Technology Nanjing, China \and
+%Xingyuan Zhang\\PLA University of Science and Technology Nanjing, China \and
+%Christian Urban\\ King's College London, United Kingdom}
 
-\markboth{C.~Wu et al.}{A Formalisation of the Myhill-Nerode Theorem based on Regular
-  Expressions}
+\author{Chunhan Wu \and Xingyuan Zhang \and Christian Urban}
+\institute{Chunhan Wu \and Xingyuan Zhang \at PLA University of Science and Technology Nanjing, China \and
+Christian Urban \at King's College London, United Kingdom}
+
+\date{Received: date / Accepted: date}
+
+%\markboth{C.~Wu et al.}{A Formalisation of the Myhill-Nerode Theorem based on Regular
+%  Expressions}
+\maketitle
+
 
 \begin{abstract} 
 There are numerous textbooks on regular languages. Many of them focus
@@ -64,17 +78,18 @@
 only regular expressions. From this theorem many closure properties of
 regular languages follow.
 \end{abstract}
-\category{F.4.1}{Mathematical Logic and Formal Languages}{Mechanical Theorem Proving}
-\category{F.4.3}{Mathematical Logic and Formal Languages}{Formal Languages}
-\terms{Interactive theorem proving, regular languages}
-\keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover}
-\begin{document}
-\begin{bottomstuff}
-Corresponding Author: Christian Urban, Department of Informatics, King's College London, 
-Strand, London WC2R 2LS, UK. Email: christian.urban@kcl.ac.uk.\\
-$^\star$This is a revised and expanded version of \cite{WuZhangUrban11}.
-\end{bottomstuff}
-\maketitle
+%\category{F.4.1}{Mathematical Logic and Formal Languages}{Mechanical Theorem Proving}
+%\category{F.4.3}{Mathematical Logic and Formal Languages}{Formal Languages}
+%\terms{Interactive theorem proving, regular languages}
+%\keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover}
+%\begin{document}
+
+%\begin{bottomstuff}
+%Corresponding Author: Christian Urban, Department of Informatics, King's College London, 
+%Strand, London WC2R 2LS, UK. Email: christian.urban@kcl.ac.uk.\\
+%$^\star$This is a revised and expanded version of \cite{WuZhangUrban11}.
+%\end{bottomstuff}
+%%\maketitle
 
 
 \input{session}