Add 2 FIXMEs
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Thu, 19 Aug 2010 15:52:36 +0900
changeset 2417 fc12e208a9e2
parent 2416 12283a96e851
child 2418 16d69f035125
Add 2 FIXMEs
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