# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1277336501 -3600
# Node ID 0d10196364aa6cbb45facf21a9bd38f7028e2975
# Parent  a0fecce8b24492f288093040d7fdb7cbf06d45f7
added comment about partial equivalence relations

diff -r a0fecce8b244 -r 0d10196364aa Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Thu Jun 24 00:27:37 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Thu Jun 24 00:41:41 2010 +0100
@@ -1134,6 +1134,9 @@
   compositions (needed for lifting theorems about @{text flat}). Also, a
   number of his definitions, like @{text ABS}, @{text REP} and @{text INJ} etc
   only exist in \cite{Homeier05} as ML-code, not included in the paper.
+  Like Homeier's, our quotient package can deal with partial equivalence
+  relations, but for lack of space we do not describe the mechanisms
+  needed for this kind of quotient constructions.
 
 
   One feature of our quotient package is that when lifting theorems, the user