--- a/Quotient-Paper/Paper.thy	Thu Aug 19 18:24:36 2010 +0800
+++ b/Quotient-Paper/Paper.thy	Fri Aug 20 16:39:39 2010 +0900
@@ -596,6 +596,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
@@ -777,6 +787,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"}
 
@@ -840,6 +857,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 +972,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.
+%%% 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 +1001,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 +1063,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