# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1282201690 -32400
# Node ID 13d93ac68b07e29664a3fd14982064912addee0d
# Parent  16d69f035125f81275e5ca5d51b31496d16f49e5
Intuition behind REL

diff -r 16d69f035125 -r 13d93ac68b07 Quotient-Paper/Paper.thy
--- 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