# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276759544 -7200
# Node ID fab7f09dda225648fd68166344ce50a44af9cadb
# Parent  0f3c497fb3b08c610aac8eb9538b7cb189a5149d
qpaper / address FIXMEs.

diff -r 0f3c497fb3b0 -r fab7f09dda22 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Thu Jun 17 07:37:26 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Thu Jun 17 09:25:44 2010 +0200
@@ -247,9 +247,7 @@
   at the beginning of this section about having to collect theorems that are
   lifted from the raw level to the quotient level into one giant list. Our
   quotient package is the first one that is modular so that it allows to lift
-%%% FIXME: First-order ones exist, for example in HOL-Light the lift_theorem function
-%%% takes all the prerequisites and one single theorem to lift.
-  single theorems separately. This has the advantage for the user of being able to develop a
+  single higher-order theorems separately. This has the advantage for the user of being able to develop a
   formal theory interactively as a natural progression. A pleasing side-result of
   the modularity is that we are able to clearly specify what is involved
   in the lifting process (this was only hinted at in \cite{Homeier05} and
@@ -396,10 +394,18 @@
   First, a general quotient theorem, like the one given in Proposition \ref{funquot},
   cannot be stated inside HOL, because of the restriction on types.
   Second, even if we were able to state such a quotient theorem, it
-  would not be true in general. However, we can prove specific and useful 
-  instances of the quotient theorem. We will 
-  show an example in Section \ref{sec:resp}.
-%%% FIXME the example is gone from the paper? Maybe we can just put it here?
+  would not be true in general. However, we can prove specific instances of a
+  quotient theorem for composing particular quotient relations.
+  To lift @{term flat} the quotient theorem for composing @{text "\<approx>\<^bsub>list\<^esub>"}
+  is necessary:
+% It says when lists are being quotiented to finite sets,
+% the contents of the lists can be quotiented as well
+ If @{term R} is an equivalence relation and @{term "Quotient R Abs Rep"} then
+
+  @{text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep o rep_fset)"}
+
+  \vspace{-.5mm}
+
 
 *}