--- a/Quotient-Paper/Paper.thy	Mon Jun 14 10:14:39 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 14 11:42:07 2010 +0200
@@ -417,7 +417,7 @@
   \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses are given below. The idea behind
   them is to recursively descend into types @{text \<sigma>} and @{text \<tau>}, and generate the appropriate
   @{text "Abs"} and @{text "Rep"} in places where the types differ. Therefore
-  we returning just the identity whenever the types are equal. All clauses
+  we return just the identity whenever the types are equal. All clauses
   are as follows:
 
   \begin{center}
@@ -706,17 +706,23 @@
   involving raw types are replaced by appropriate aggregate
   relations. It is defined as follows:
 
-  \begin{itemize}
-  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"}
-  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
-  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"}
-  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
-  \item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"}
-  \item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"}
-  \item @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}
-  \item @{text "REG (v\<^isub>1, v\<^isub>2) = v\<^isub>1"}
-  \item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"}
-  \end{itemize}
+  \begin{center}
+  \begin{tabular}{rcl}
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\
+  @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma>. REG (t, s)"}\\
+  @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\
+  @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma>. REG (t, s)"}\\
+  @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{equality (with same types and different types):}\\
+  @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>)"} & $\dn$ & @{text "(op =) : \<sigma>"}\\
+  @{text "REG ((op =) : \<sigma>, (op =) : \<tau>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>) : \<sigma>"}\\
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{application, variable, constant:}\\
+  @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} & $\dn$ & @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\
+  @{text "REG (v\<^isub>1, v\<^isub>2)"} & $\dn$ & @{text "v\<^isub>1"}\\
+  @{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\
+  \end{tabular}
+  \end{center}
 
   In the above definition we omitted the cases for existential quantifiers
   and unique existential quantifiers, as they are very similar to the cases