--- a/Quotient-Paper/Paper.thy	Mon Jun 14 09:16:22 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 14 09:28:52 2010 +0200
@@ -655,7 +655,7 @@
   when we compose the quotient with itself, as there is no simple
   intermediate step.
 
-  Lets take again the example of @{term concat}. To be able to lift
+  Lets take again the example of @{term flat}. To be able to lift
   theorems that talk about it we provide the composition quotient
   theorems, which then lets us perform the lifting procedure in an
   unchanged way:
@@ -746,8 +746,9 @@
 
 subsection {* Proof procedure *}
 
-(* In the below the type-guiding 'QuotTrue' assumption is removed; since we
-   present in a paper a version with typed-variables it is not necessary *)
+(* In the below the type-guiding 'QuotTrue' assumption is removed. We need it
+   only for bound variables without types, while in the paper presentation
+   variables are typed *)
 
 text {*
 
@@ -771,12 +772,12 @@
   respectfulness and preservation theorems are given. It is not the case
   with regularization; sometimes a theorem given by the user does not
   imply a regularized version and a stronger one needs to be proved. This
-  is outside of the scope of the quotient package, so the user is then left
-  with such obligations. As an example lets see the simplest possible
-  non-liftable theorem for integers: When we want to prove @{term "0 \<noteq> 1"}
-  on integers the fact that @{term "\<not> (0, 0) = (1, 0)"} is not enough. It
-  only shows that particular items in the equivalence classes are not equal,
-  a more general statement saying that the classes are not equal is necessary.
+  is outside of the scope of the quotient package, so such obligations are
+  left to the user. Take a simple statement for integers @{term "0 \<noteq> 1"}.
+  It does not follow from the fact that @{term "\<not> (0, 0) = (1, 0)"} because
+  of regularization. The raw theorem only shows that particular items in the
+  equivalence classes are not equal. A more general statement saying that
+  the classes are not equal is necessary.
 *}
 
 subsection {* Proving Regularization *}
@@ -787,7 +788,7 @@
   of similar statements into simpler implication subgoals. These are enhanced
   with special quotient theorem in the regularization goal. Below we only show
   the versions for the universal quantifier. For the existential quantifier
-  and abstraction they are analogous with some symmetry.
+  and abstraction they are analogous.
 
   First, bounded universal quantifiers can be removed on the right:
 
@@ -801,10 +802,10 @@
 
   @{thm [display, indent=10] (concl) ball_reg_eqv_range[no_vars]}
 
-  The last theorem is new in comparison with Homeier's package, there the
+  The last theorem is new in comparison with Homeier's package. There the
   injection procedure would be used to prove goals with such shape, and there
-  the equivalence assumption would be useful. We use it directly also for
-  composed relations where the range type is a type for which we know an
+  the equivalence assumption would be used. We use the above theorem directly
+  also for composed relations where the range type is a type for which we know an
   equivalence theorem. This allows separating regularization from injection.
 
 *}
@@ -823,11 +824,11 @@
 text {*
   The injection proof starts with an equality between the regularized theorem
   and the injected version. The proof again follows by the structure of the
-  two term, and is defined for a goal being a relation between the two terms.
+  two terms, and is defined for a goal being a relation between these two terms.
 
   \begin{itemize}
   \item For two constants, an appropriate constant respectfullness assumption is used.
-  \item For two variables, the regularization assumptions state that they are related.
+  \item For two variables, we use the assumptions proved in regularization.
   \item For two abstractions, they are eta-expanded and beta-reduced.
   \end{itemize}