diff -r cd694a9988bc -r f5cbf74d4ec5 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Fri Aug 20 16:50:46 2010 +0900
+++ b/Quotient-Paper/Paper.thy	Fri Aug 20 16:55:58 2010 +0900
@@ -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);
@@ -987,8 +990,8 @@
 %%% 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?
+%%% 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