# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1282200756 -32400
# Node ID fc12e208a9e28ba770cd83b5a211437383e18d33
# Parent  12283a96e85123bc35d38c16952717e0ca15a7b4
Add 2 FIXMEs

diff -r 12283a96e851 -r fc12e208a9e2 Quotient-Paper/Paper.thy
--- 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