--- a/Quotient-Paper/Paper.thy	Wed Aug 18 00:23:42 2010 +0800
+++ b/Quotient-Paper/Paper.thy	Thu Aug 19 13:00:49 2010 +0900
@@ -214,7 +214,7 @@
   where we take the representation of the arguments @{text n} and @{text m},
   add them according to the function @{text "add_pair"} and then take the
   abstraction of the result.  This is all straightforward and the existing
-  quotient packages can deal with such definitions. But what is surprising
+  quotient packages can deal with such definitions. But what is surprising is
   that none of them can deal with slightly more complicated definitions involving
   \emph{compositions} of quotients. Such compositions are needed for example
   in case of quotienting lists to yield finite sets and the operator that 
@@ -729,9 +729,9 @@
   \noindent
   and the point is that the user cannot discharge it: because it is not true. To see this,
   we can just unfold the definition of @{text "\<doublearr>"} \eqref{relfun} 
-  using extensionally to obtain the false statement
+  using extensionality to obtain the false statement
 
-  @{text [display, indent=10] "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 implies bn(t\<^isub>1) = bn(t\<^isub>2)"}
+  @{text [display, indent=10] "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 then bn(t\<^isub>1) = bn(t\<^isub>2)"}
  
   \noindent
   In contrast, if we lift a theorem about @{text "append"} to a theorem describing 
@@ -816,7 +816,7 @@
   \emph{injection} and \emph{cleaning} according to procedures in Homeier's ML-code.
 
   The purpose of regularization is to change the quantifiers and abstractions
-  in a ``raw'' theorem to quantifiers over variables that respect the relation
+  in a ``raw'' theorem to quantifiers over variables that respect their respective relations
   (Definition \ref{def:respects} states what respects means). The purpose of injection is to add @{term Rep}
   and @{term Abs} of appropriate types in front of constants and variables
   of the raw type so that they can be replaced by the corresponding constants from the
@@ -953,7 +953,7 @@
   @{text [display, indent=10] "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}    
 
   \noindent
-  If @{term R\<^isub>2} is an equivalence relation, we can prove
+  If @{term R\<^isub>2} is an equivalence relation, we can prove that for any predicate @{term P}
 
   @{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
 
@@ -964,7 +964,8 @@
   because this allows us to completely separate the first and the second
   proof step into two independent ``units''.
 
-  The second proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"},  starts with an equality. 
+  The second proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"},  starts with an equality
+  between the terms of the regularized theorem and the injected theorem.
   The proof again follows the structure of the
   two underlying terms and is defined for a goal being a relation between these two terms.
 
@@ -987,8 +988,8 @@
   We defined the theorem @{text "inj_thm"} in such a way that
   establishing the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be
   achieved by rewriting @{text "inj_thm"} with the preservation theorems and quotient
-  definitions. Then for all lifted constants, their definitions
-  are used to fold the @{term Rep} with the raw constant. Next for
+  definitions. Next the definitions of all lifted constants
+  are used to fold the @{term Rep} with the raw constants. Next for
   all abstractions and quantifiers the lambda and
   quantifier preservation theorems are used to replace the
   variables that include raw types with respects by quantifiers
@@ -999,8 +1000,9 @@
   @{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
 
   \noindent
-  Next, relations over lifted types are folded to equalities.
-  For this the following theorem has been shown by  Homeier~\cite{Homeier05}:
+  Next, relations over lifted types can be rewritten to equalities
+  over lifted type. Rewriting is performed with the following theorem,
+  which has been shown by Homeier~\cite{Homeier05}:
 
   @{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]}