--- a/Journal/document/root.tex	Tue Jul 26 10:58:26 2011 +0000
+++ b/Journal/document/root.tex	Tue Jul 26 18:12:07 2011 +0000
@@ -22,6 +22,9 @@
 \renewcommand{\isastyleminor}{\it}%
 \renewcommand{\isastyle}{\normalsize\it}%
 
+\newcommand*{\threesim}{%
+  \mathrel{\vcenter{\offinterlineskip
+  \hbox{$\sim$}\vskip-.35ex\hbox{$\sim$}\vskip-.35ex\hbox{$\sim$}}}}
 
 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
 \renewcommand{\isasymequiv}{$\dn$}
@@ -36,10 +39,13 @@
 
 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular
   Expressions}
+\thanks{This is a revised and expanded version of ???}
 \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}
+\subjclass{68Q45}
+\keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover}
 
 \begin{abstract} 
 There are numerous textbooks on regular languages. Nearly all of them