# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276572770 -7200
# Node ID 85291ef50354040910d800829fb00a05213c763a
# Parent  72ce58b76c3b1786801bca21d7753809bca0907c
qpaper/related work

diff -r 72ce58b76c3b -r 85291ef50354 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Tue Jun 15 02:03:18 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue Jun 15 05:32:50 2010 +0200
@@ -879,7 +879,7 @@
 
   @{thm [display, indent=10] ball_reg_eqv[no_vars]}
 
-  And finally it can be removed anywhere if @{term R2} is an equivalence relation, then:
+  And finally it can be removed anywhere if @{term R2} is an equivalence relation:
 
   @{thm [display, indent=10] (concl) ball_reg_eqv_range[no_vars]}
 
@@ -1030,31 +1030,18 @@
 section {* Conclusion and Related Work\label{sec:conc}*}
 
 text {*
-  
-\begin{itemize}
-
-  \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 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~\cite{Slotosch97}.
+  Oscar Slotosch~\cite{Slotosch97} implemented a mechanism that automatically
+  defines quotient types for Isabelle/HOL. It did not include theorem lifting.
+  John Harrison's quotient package~\cite{harrison-thesis} is the first one to
+  lift theorems, however only first order. There is work on quotient types in
+  non-HOL based systems and logical frameworks, namely theory interpretations
+  in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or
+  the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}.
+  Larry Paulson shows a construction of quotients that does not require the
+  Hilbert Choice operator, again only first order~\cite{Paulson06}.
 
-  \item PER. And how to avoid it.
-
-  \item Necessity of Hilbert Choice op and Larry's quotients~\cite{Paulson06}
-
-  \item Setoids in Coq and \cite{ChicliPS02}
-
-  \end{itemize}
-
+  The closest to our package is the package for HOL4 by Peter Homeier~\cite{Homeier05}...
 
   The code of the quotient package described here is already included in the
   standard distribution of Isabelle.\footnote{Available from