# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1274175979 -7200
# Node ID 3c4eff4a73daf94d591c802e87861f6aa1ff7c92
# Parent  d7d4491535a9c74e1cde6846993404fac92525fc# Parent  ad608532c7cd2b48fbbfb32051c8244e66c5edd7
merge

diff -r ad608532c7cd -r 3c4eff4a73da Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Mon May 17 20:23:40 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Tue May 18 11:46:19 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}
 *}