--- a/Quotient-Paper/Paper.thy	Sun Aug 22 11:00:53 2010 +0800
+++ b/Quotient-Paper/Paper.thy	Sun Aug 22 12:36:53 2010 +0800
@@ -152,6 +152,9 @@
 %%% Secondly, isn't the _set of_ equivalence classes mapped to and from the new type?
 %%% Thirdly, what do the words "non-empty subset" refer to ?
 
+%%% Cezary: I like the diagram, maybe 'new type' could be outside, but otherwise
+%%% I wouldn't change it.
+
   \begin{center}
   \mbox{}\hspace{20mm}\begin{tikzpicture}
   %%\draw[step=2mm] (-4,-1) grid (4,1);
@@ -596,6 +599,16 @@
   In this case @{text MAP} generates  the 
   aggregate map-function:
 
+%%% FIXME: Reviewer 2 asks: last two lines defining ABS and REP for
+%%% unequal type constructors: How are the $\varrho$s defined? The
+%%% following paragraph mentions them, but this paragraph is unclear,
+%%% since it then mentions $\alpha$s, which do not seem to be defined
+%%% either. As a result, I do not understand the first two sentences
+%%% in this paragraph. I can imagine roughly what the following
+%%% sentence `The $\sigma$s' are given by the matchers for the
+%%% $\alpha$s$ when matching $\varrho$s $\kappa$ against $\sigma$s
+%%% $\kappa$.' means, but also think that it is too vague.
+
   @{text [display, indent=10] "\<lambda>a b. map_prod (map_list a) b"}
   
   \noindent
@@ -693,6 +706,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
@@ -777,6 +793,13 @@
   and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"}, then a
   preservation property is as follows
 
+%%% FIXME: Reviewer 2 asks: You say what a preservation theorem is,
+%%% but not which preservation theorems you assume. Do you generate a
+%%% proof obligation for a preservation theorem for each raw constant
+%%% and its corresponding lifted constant?
+
+%%% Cezary: I think this would be a nice thing to do but we have not
+%%% done it, the theorems need to be 'guessed' from the remaining obligations
 
   @{text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies  ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"}
 
@@ -826,6 +849,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},
@@ -840,6 +869,10 @@
   first two phases into the form the user has specified. Abstractly, our
   package establishes the following three proof steps:
 
+%%% FIXME: Reviewer 1 complains that the reader needs to guess the
+%%% meaning of reg_thm and inj_thm, as well as the arguments of REG
+%%% which are given above. I wouldn't change it.
+
   \begin{center}
   \begin{tabular}{l@ {\hspace{4mm}}l}
   1.) Regularization & @{text "raw_thm \<longrightarrow> reg_thm"}\\
@@ -951,6 +984,15 @@
   In this definition we again omitted the cases for existential and unique existential
   quantifiers. 
 
+%%% FIXME: Reviewer2 citing following sentence: You mention earlier
+%%% that this implication may fail to be true. Does that meant that
+%%% the `first proof step' is a heuristic that proves the implication
+%%% raw_thm \implies reg_thm in some instances, but fails in others?
+%%% You should clarify under which circumstances the implication is
+%%% being proved here.
+%%% Cezary: It would be nice to cite Homeiers discussions in the
+%%% Quotient Package manual from HOL (the longer paper), do you agree?
+
   In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always 
   start with an implication. Isabelle provides \emph{mono} rules that can split up 
   the implications into simpler implicational subgoals. This succeeds for every
@@ -971,6 +1013,9 @@
   \noindent
   If @{term R\<^isub>2} is an equivalence relation, we can prove that for any predicate @{term P}
 
+%%% FIXME Reviewer 1 claims the theorem is obviously false so maybe we
+%%% should include a proof sketch?
+
   @{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
 
   \noindent
@@ -1030,9 +1075,11 @@
 
 section {* Examples \label{sec:examples} *}
 
-(* Mention why equivalence *)
+text {*
 
-text {*
+%%% FIXME Reviewer 1 would like an example of regularized and injected
+%%% statements. He asks for the examples twice, but I would still ignore
+%%% it due to lack of space...
 
   In this section we will show a sequence of declarations for defining the 
   type of integers by quotienting pairs of natural numbers, and
@@ -1161,6 +1208,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