--- a/Journal/Paper.thy	Thu Jul 28 14:22:10 2011 +0000
+++ b/Journal/Paper.thy	Thu Jul 28 17:52:36 2011 +0000
@@ -67,7 +67,8 @@
   tag_str_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100) and
   tag_eq_rel ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and
   Delta ("\<Delta>'(_')") and
-  nullable ("\<delta>'(_')")
+  nullable ("\<delta>'(_')") and
+  Cons ("_ :: _" [100, 100] 100)
 
 lemma meta_eq_app:
   shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
@@ -389,7 +390,7 @@
   
   \begin{prpstn}\label{langprops}\mbox{}\\
   \begin{tabular}{@ {}ll}
-  (i)   & @{thm star_cases}     \\ 
+  (i)   & @{thm star_unfold_left}     \\ 
   (ii)  & @{thm[mode=IfThen] pow_length}\\
   (iii) & @{thm conc_Union_left} \\ 
   \end{tabular}
@@ -1098,8 +1099,38 @@
   Much more interesting, however, are the inductive cases. They seem hard to solve 
   directly. The reader is invited to try. 
 
-  Constable et al \cite{Constable00} give the following suggestive picture about
-  equivalence classes:
+  In order how to see how our first proof proceeds we use the following suggestive picture 
+  from Constable et al \cite{Constable00}:
+
+  \begin{center}
+  \begin{tabular}{c@ {\hspace{10mm}}c@ {\hspace{10mm}}c}
+  \begin{tikzpicture}[scale=1]
+  %Circle
+  \draw[thick] (0,0) circle (1.1);    
+  \end{tikzpicture}
+  &
+  \begin{tikzpicture}[scale=1]
+  %Circle
+  \draw[thick] (0,0) circle (1.1);    
+  %Main rays
+  \foreach \a in {0, 90,...,359}
+    \draw[very thick] (0, 0) -- (\a:1.1);
+  \foreach \a / \l in {45/1, 135/2, 225/3, 315/4}
+      \draw (\a: 0.65) node {$a_\l$};
+  \end{tikzpicture}
+  &
+  \begin{tikzpicture}[scale=1]
+  %Circle
+  \draw[thick] (0,0) circle (1.1);    
+  %Main rays
+  \foreach \a in {0, 45,...,359}
+     \draw[very thick] (0, 0) -- (\a:1.1);
+  \foreach \a / \l in {22.5/1.1, 67.5/1.2, 112.5/2.1, 157.5/2.2, 202.4/3.1, 247.5/3.2, 292.5/4.1, 337.5/4.2}
+      \draw (\a: 0.77) node {$a_{\l}$};
+  \end{tikzpicture}\\
+  @{term UNIV} & @{term "UNIV // (\<approx>(lang r))"} & @{term "UNIV // R"}
+  \end{tabular}
+  \end{center}
 
   Our first proof will rely on some
   \emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will