--- a/Quotient-Paper/Paper.thy	Thu Aug 19 16:05:31 2010 +0900
+++ b/Quotient-Paper/Paper.thy	Thu Aug 19 16:08:10 2010 +0900
@@ -694,7 +694,11 @@
   compositions. 
 
   To formally define what respectfulness is, we have to first define 
-  the notion of \emph{aggregate equivalence relations} using the function @{text REL}:
+  the notion of \emph{aggregate equivalence relations} using the function @{text "REL(\<sigma>, \<tau>)"}
+  The idea behind this function is to simultaneously descend into the raw types
+  @{text \<sigma>} and quotient types @{text \<tau>}, and generate the appropriate
+  quotient equivalence relations in places where the types differ and equalities
+  elsewhere.
 
   \begin{center}
   \hfill