--- 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