# HG changeset patch
# User urbanc
# Date 1297194863 0
# Node ID f438f4dbaada30d2b73a956bbd95b79706700cfa
# Parent  14b12b5de6d36f3ce37dfa8bea90d3112c6e6d44
a bit more on the paper

diff -r 14b12b5de6d3 -r f438f4dbaada Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Feb 08 18:04:54 2011 +0000
+++ b/Paper/Paper.thy	Tue Feb 08 19:54:23 2011 +0000
@@ -400,14 +400,14 @@
   we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations
   %
   \begin{equation}\label{inv1}
-  @{text "X\<^isub>i = L(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> L(Y\<^isub>i\<^isub>q, CHAR c\<^isub>i\<^isub>q)"}.
+  @{text "X\<^isub>i = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>q, CHAR c\<^isub>i\<^isub>q)"}.
   \end{equation}
 
   \noindent
   hold. Similarly for @{text "X\<^isub>1"} we can show the following equation
   %
   \begin{equation}\label{inv2}
-  @{text "X\<^isub>1 = L(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> L(Y\<^isub>i\<^isub>p, CHAR c\<^isub>i\<^isub>p) \<union> L(\<lambda>(EMPTY))"}.
+  @{text "X\<^isub>1 = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>p, CHAR c\<^isub>i\<^isub>p) \<union> \<calL>(\<lambda>(EMPTY))"}.
   \end{equation}
 
   \noindent
diff -r 14b12b5de6d3 -r f438f4dbaada Paper/document/root.tex
--- a/Paper/document/root.tex	Tue Feb 08 18:04:54 2011 +0000
+++ b/Paper/document/root.tex	Tue Feb 08 19:54:23 2011 +0000
@@ -22,7 +22,7 @@
 \renewcommand{\isasymemptyset}{$\varnothing$}
 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
 
-
+\newcommand{\isasymcalL}{\ensuremath{\cal{L}}}
 \begin{document}
 
 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular