--- a/Quotient-Paper/Paper.thy	Mon May 17 17:34:02 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue May 18 11:45:49 2010 +0200
@@ -134,7 +134,7 @@
 
 Example of non-regularizable theorem ($0 = 1$).
 
-New regularization lemmas:
+Separtion of regularization from injection thanks to the following 2 lemmas:
 \begin{lemma}
 If @{term R2} is an equivalence relation, then:
 \begin{eqnarray}
@@ -159,20 +159,23 @@
 text {*
   \begin{itemize}
 
-  \item Peter Homeier's package (and related work from there), John
-    Harrison's one.
+  \item Peter Homeier's package~\cite{Homeier05} (and related work from there)
+  \item John Harrison's one~\cite{harrison-thesis} is the first one to lift theorems
+    but only first order.
 
-  \item Manually defined quotients in Isabelle/HOL Library (Larry's
-    quotients, Markus's Quotient\_Type, Dixon's FSet, \ldots)
+  \item PVS~\cite{PVS:Interpretations}
+  \item MetaPRL~\cite{Nogin02}
+  \item Manually defined quotients in Isabelle/HOL Library (Markus's Quotient\_Type,
+    Dixon's FSet, \ldots)
 
   \item Oscar Slotosch defines quotient-type automatically but no
-    lifting.
+    lifting~\cite{Slotosch97}.
 
   \item PER. And how to avoid it.
 
-  \item Necessity of Hilbert Choice op.
+  \item Necessity of Hilbert Choice op and Larry's quotients~\cite{Paulson06}
 
-  \item Setoids in Coq
+  \item Setoids in Coq and \cite{ChicliPS02}
 
   \end{itemize}
 *}