# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1282290646 -32400
# Node ID cd694a9988bce4a4a395bcf81d230b058ce18ca1
# Parent  4ef4661be8158417002a0cc86e8ef2be8a86514e
Finished adding remarks from the reviewers.

diff -r 4ef4661be815 -r cd694a9988bc Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Fri Aug 20 16:39:39 2010 +0900
+++ b/Quotient-Paper/Paper.thy	Fri Aug 20 16:50:46 2010 +0900
@@ -703,6 +703,9 @@
   to slightly extend Homeier's definitions in order to deal with quotient
   compositions. 
 
+%%% FIXME: Reviewer 3 asks why are the definitions that follow enough to deal
+%%% with quotient composition.
+
   To formally define what respectfulness is, we have to first define 
   the notion of \emph{aggregate equivalence relations} using the function @{text "REL(\<sigma>, \<tau>)"}
   The idea behind this function is to simultaneously descend into the raw types
@@ -843,6 +846,12 @@
 
 text {*
 
+%%% FIXME Reviewer 3 asks: Section 5 shows the technicalities of
+%%% lifting theorems. But there is no clarification about the
+%%% correctness. A reader would also be interested in seeing some
+%%% discussions about the generality and limitation of the approach
+%%% proposed there
+
   The main benefit of a quotient package is to lift automatically theorems over raw
   types to theorems over quotient types. We will perform this lifting in
   three phases, called \emph{regularization},
@@ -1196,6 +1205,8 @@
   relations, but for lack of space we do not describe the mechanisms
   needed for this kind of quotient constructions.
 
+%%% FIXME Reviewer 3 would like to know more about the lifting in Coq and PVS,
+%%% and some comparison. I don't think we have the space for any additions...
 
   One feature of our quotient package is that when lifting theorems, the user
   can precisely specify what the lifted theorem should look like. This feature