--- a/Quotient-Paper/Paper.thy	Thu Aug 19 13:00:49 2010 +0900
+++ b/Quotient-Paper/Paper.thy	Thu Aug 19 13:58:47 2010 +0900
@@ -332,7 +332,10 @@
   Using extensionality and unfolding the definition of @{text "\<singlearr>"}, 
   we can get back to \eqref{adddef}. 
   In what follows we shall use the convention to write @{text "map_\<kappa>"} for a map-function 
-  of the type-constructor @{text \<kappa>}. In our implementation we maintain 
+  of the type-constructor @{text \<kappa>}. For a type @{text \<kappa>} with arguments @{text "\<alpha>\<^isub>1\<^isub>\<dots>\<^isub>n"} the
+  type of @{text "map_\<kappa>"} has to be @{text "\<alpha>\<^isub>1\<Rightarrow>\<dots>\<Rightarrow>\<alpha>\<^isub>n\<Rightarrow>\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>n \<kappa>"}. For example @{text "map_list"}
+  has to have the type @{text "\<alpha>\<Rightarrow>\<alpha> list"}.
+  In our implementation we maintain
   a database of these map-functions that can be dynamically extended.
 
   It will also be necessary to have operators, referred to as @{text "rel_\<kappa>"},
@@ -371,7 +374,7 @@
   \begin{definition}[Quotient Types]
   Given a relation $R$, an abstraction function $Abs$
   and a representation function $Rep$, the predicate @{term "Quotient R Abs Rep"}
-  means
+  holds if and only if
   \begin{enumerate}
   \item @{thm (rhs1) Quotient_def[of "R", no_vars]}
   \item @{thm (rhs2) Quotient_def[of "R", no_vars]}
@@ -407,12 +410,10 @@
   \end{definition}
 
   \noindent
-  Unfortunately, there are two predicaments with compositions of relations.
-  First, a general quotient theorem for @{text "\<circ>\<circ>\<circ>"}, like the one for @{text "\<singlearr>"} 
-  given in Proposition \ref{funquot},
-  cannot be stated inside HOL, because of restrictions on types.
-  Second, even if we were able to state such a quotient theorem, it
-  would not be true in general. However, we can prove specific instances of a
+  Unfortunately a general quotient theorem for @{text "\<circ>\<circ>\<circ>"}, analogous to the one
+  for @{text "\<singlearr>"} given in Proposition \ref{funquot}, would not be true
+  in general. It cannot even be stated inside HOL, because of restrictions on types.
+  However, we can prove specific instances of a
   quotient theorem for composing particular quotient relations.
   For example, to lift theorems involving @{term flat} the quotient theorem for 
   composing @{text "\<approx>\<^bsub>list\<^esub>"} will be necessary: given @{term "Quotient R Abs Rep"} 
@@ -521,7 +522,7 @@
   building unions of finite sets (@{text "flat"} having the type 
   @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"}). 
 
-  The problem for us is that from such declarations we need to derive proper
+  From such declarations given by the user, the quotient package needs to derive proper
   definitions using @{text "Abs"} and @{text "Rep"}. The data we rely on is the given quotient type
   @{text "\<tau>"} and the raw type @{text "\<sigma>"}.  They allow us to define \emph{aggregate
   abstraction} and \emph{representation functions} using the functions @{text "ABS (\<sigma>,
@@ -1066,9 +1067,9 @@
   \end{isabelle}
 
   \noindent
-  If the user lifts this theorem, all proof obligations are 
-  automatically discharged, except the respectfulness
-  proof for @{text "add_pair"}:
+  If the user lifts this theorem, the quotient package performs all the lifting
+  automatically leaving the respectfulness proof for the constant @{text "add_pair"}
+  as the only remaining proof obligation. This property needs to be proved by the user:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
   \begin{tabular}{@ {}l}
@@ -1078,8 +1079,7 @@
   \end{isabelle}
 
   \noindent
-  This property needs to be proved by the user. It
-  can be discharged automatically by Isabelle when hinting to unfold the definition
+  It can be discharged automatically by Isabelle when hinting to unfold the definition
   of @{text "\<doublearr>"}.
   After this, the user can prove the lifted lemma as follows: