# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276573401 -7200
# Node ID 600f6cb82e941e0be9bd7ad2a2836624c4be5a85
# Parent  85291ef50354040910d800829fb00a05213c763a
qpaper / hol4

diff -r 85291ef50354 -r 600f6cb82e94 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Tue Jun 15 05:32:50 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue Jun 15 05:43:21 2010 +0200
@@ -1041,7 +1041,15 @@
   Larry Paulson shows a construction of quotients that does not require the
   Hilbert Choice operator, again only first order~\cite{Paulson06}.
 
-  The closest to our package is the package for HOL4 by Peter Homeier~\cite{Homeier05}...
+  The closest to our package is the package for HOL4 by Peter Homeier~\cite{Homeier05},
+  which is the first one to support lifting of higher order theorems. In
+  comparison with this package we explore the notion of composition of quotients,
+  which allows lifting constants like @{term "concat"} and theorems about it.
+  The HOL4 package requires a big lists of constants, theorems to lift,
+  respectfullness conditions as input. Our package is modularized, so that
+  single definitions, single theorems or single respectfullness conditions etc
+  can be added, which allows a natural use of the quotient package together
+  with type-classes and locales.
 
   The code of the quotient package described here is already included in the
   standard distribution of Isabelle.\footnote{Available from