--- 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