--- a/Journal/document/root.tex	Fri Apr 20 14:15:36 2012 +0000
+++ b/Journal/document/root.tex	Mon Apr 23 08:01:37 2012 +0000
@@ -1,4 +1,4 @@
-\documentclass[acmtocl]{acmtrans2m}
+\documentclass[acmtocl,final]{acmtrans2m}
 \usepackage{isabelle}
 \usepackage{isabellesym}
 \usepackage{amsmath}
@@ -9,7 +9,7 @@
 \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}
@@ -48,22 +48,21 @@
 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}
+
 \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 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.
+There are numerous textbooks on regular languages. Many of them focus
+on finite automata for proving properties.  Unfortunately, automata
+are not so straightforward to formalise in theorem provers. The reason
+is that natural representations for automata are graphs, matrices or
+functions, none of which are inductive datatypes. Regular
+expressions can be defined straightforwardly as a datatype and a
+corresponding reasoning infrastructure comes for free in theorem
+provers. 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}