--- a/Paper/document/root.tex	Wed Feb 09 07:27:30 2011 +0000
+++ b/Paper/document/root.tex	Wed Feb 09 09:46:59 2011 +0000
@@ -9,9 +9,8 @@
 \usepackage{ot1patch}
 \usepackage{times}
 \usepackage{proof}
+%%\usepackage{mathabx}
 \usepackage{stmaryrd}
-\usepackage{mathabx}
-
 
 \urlstyle{rm}
 \isabellestyle{it}
@@ -25,6 +24,9 @@
 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
 
 \newcommand{\isasymcalL}{\ensuremath{\cal{L}}}
+\newcommand{\isasymbigplus}{\ensuremath{\bigplus}}
+
+\newcommand{\bigplus}{\mbox{\large\bf$+$}}
 \begin{document}
 
 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular