--- a/Quotient-Paper/Paper.thy Thu Aug 19 15:46:28 2010 +0900
+++ b/Quotient-Paper/Paper.thy Thu Aug 19 15:52:36 2010 +0900
@@ -147,6 +147,11 @@
\cite{Homeier05} implemented in HOL4. The fundamental construction these
quotient packages perform can be illustrated by the following picture:
+%%% FIXME: Referee 1 says:
+%%% Diagram is unclear. Firstly, isn't an existing type a "set (not sets) of raw elements"?
+%%% 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 ?
+
\begin{center}
\mbox{}\hspace{20mm}\begin{tikzpicture}
%%\draw[step=2mm] (-4,-1) grid (4,1);
@@ -404,6 +409,9 @@
use of this part of Homeier's work including an extension
for dealing with compositions of equivalence relations defined as follows:
+%%% FIXME Referee 2 claims that composition-of-relations means OO, and this is also
+%%% what wikipedia says. Any idea for a different name? Conjugation of Relations?
+
\begin{definition}[Composition of Relations]
@{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate
composition defined by