# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1274175949 -7200
# Node ID d7d4491535a9c74e1cde6846993404fac92525fc
# Parent  270207489062bca8e50d6a75e0f0c35a5f19d317
starting bibliography

diff -r 270207489062 -r d7d4491535a9 Quotient-Paper/Paper.thy
--- 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}
 *}