--- a/Quotient-Paper/Paper.thy	Wed Jun 16 03:44:10 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Wed Jun 16 03:47:38 2010 +0100
@@ -711,7 +711,7 @@
   \noindent
   and 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 extensionality to obtain
+  using extensionally to obtain
 
   @{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)"}
  
@@ -740,7 +740,7 @@
   is to become an integer. But we still want to use @{text cons} for
   adding integers to lists---just with a different type. 
   To be able to lift such theorems, we need a \emph{preservation theorem} 
-  for @{text cons}. Assuming we have a poplymorphic raw constant 
+  for @{text cons}. Assuming we have a polymorphic raw constant 
   @{text "c\<^isub>r :: \<sigma>"} and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"}, 
   then a preservation theorem is as follows
 
@@ -799,11 +799,11 @@
 
 text {*
 
-  The core of a quotient package lifts an original theorem to a lifted
-  version. We will perform this operation in three phases. In the
-  following we call these phases \emph{regularization},
-  \emph{injection} and \emph{cleaning} following the names used in
-  Homeier's HOL4 implementation.
+  The main purpose of the quotient package is to lifts an theorem over raw
+  types to a theorem over quotient types. We will perform this operation in
+  three phases. In the following we call these phases \emph{regularization},
+  \emph{injection} and \emph{cleaning} following the names Homeier used
+  in his implementation.
 
   Regularization is supposed to change the quantifications and abstractions
   in the theorem to quantification over variables that respect the relation