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