diff -r 73127f5db18f -r bea94f1e6771 Journal/document/root.tex
--- a/Journal/document/root.tex	Fri Apr 20 11:27:49 2012 +0000
+++ b/Journal/document/root.tex	Fri Apr 20 11:45:06 2012 +0000
@@ -1,4 +1,4 @@
-\documentclass{ita}
+\documentclass[acmtocl]{acmtrans2m}
 \usepackage{isabelle}
 \usepackage{isabellesym}
 \usepackage{amsmath}
@@ -9,13 +9,12 @@
 \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{proof}
-%%\usepackage{mathabx}
 \usepackage{stmaryrd}
 \usepackage{mathpartir}
+\usepackage{longtable}
 
 \urlstyle{rm}
 \isabellestyle{it}
@@ -35,39 +34,52 @@
 \newcommand{\isasymbigplus}{\ensuremath{\bigplus}}
 
 \newcommand{\bigplus}{\mbox{\Large\bf$+$}}
-\begin{document}
+
+\newtheorem{thrm}{Theorem}[section]
+\newtheorem{lmm}{Lemma}[section]
+\newtheorem{dfntn}{Definition}[section]
+\newtheorem{prpstn}{Proposition}[section]
+
 
 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular
-  Expressions}
-\thanks{This is a revised and expanded version of \cite{WuZhangUrban11}.}
-\author{Chunhan Wu}\address{PLA University of Science and Technology, China}
-\author{Xingyuan Zhang}\sameaddress{1}
-\author{Christian Urban}\address{King's College London, United Kingdom}\secondaddress{corresponding author}
-\subjclass{68Q45}
-\keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover}
+  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}
 
 \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
-side a connection with regular expressions. Unfortunately, automata are difficult
-to formalise in HOL-based theorem provers. The reason is that
-they need to be represented as graphs, matrices or functions, none of which
-are inductive datatypes. Also convenient operations for disjoint unions of
-graphs, matrices and functions are not easily formalisiable in HOL. In contrast, regular
-expressions can be defined conveniently as a datatype and a corresponding
-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. From this theorem many closure
-properties of regular languages follow.
+introduce the subject by describing finite automata and only
+mentioning on the side a connection with regular
+expressions. Unfortunately, automata are not so straightforward to
+formalise in theorem provers. The reason is that a natural
+representation for automata are graphs, matrices or functions, none of
+which are inductive datatypes. Also convenient operations for disjoint
+unions of graphs, matrices and functions are not easily formalisiable
+in Isabelle/HOL, the theorem prover we are using. In contrast, regular
+expressions can be defined conveniently as a datatype and a
+corresponding 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. 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
 
+
 \input{session}
 
-%%\mbox{}\\[-10mm]
-\bibliographystyle{plain}
-\bibliography{root}
-
 \end{document}
 
 %%% Local Variables: