--- a/Quotient-Paper/Paper.thy	Mon Jun 14 14:45:40 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 14 15:16:42 2010 +0200
@@ -686,23 +686,20 @@
 section {* Lifting of Theorems *}
 
 text {*
-  The core of the quotient package takes an original theorem that
-  talks about the raw types, and the statement of the theorem that
-  it is supposed to produce. This is different from other existing
-  quotient packages, where only the raw theorems were necessary.
-  We notice that in some cases only some occurrences of the raw
-  types need to be lifted. This is for example the case in the
-  new Nominal package, where a raw datatype that talks about
-  pairs of natural numbers or strings (being lists of characters)
-  should not be changed to a quotient datatype with constructors
-  taking integers or finite sets of characters. To simplify the
-  use of the quotient package we additionally provide an automated
-  statement translation mechanism that replaces occurrences of
-  types that match given quotients by appropriate lifted types.
+  The core of our quotient package takes an original theorem that
+  talks about the raw types and the statement of the theorem that
+  it is supposed to produce. This is different from existing
+  quotient packages, where only the raw theorems are necessary.
+  To simplify the use of the quotient package we additionally provide
+  an automated statement translation mechanism which can optionally
+  take a list of quotient types. It is possible that a user wants
+  to lift only some occurrences of a quotiented type. In this case
+  the user specifies the complete lifted goal instead of using the
+  automated mechanism.
 
   Lifting the theorems is performed in three steps. In the following
   we call these steps \emph{regularization}, \emph{injection} and
-  \emph{cleaning} following the names used in Homeier's HOL
+  \emph{cleaning} following the names used in Homeier's HOL4
   implementation.
 
   We first define the statement of the regularized theorem based
@@ -717,13 +714,13 @@
 
 text {*
 
-  We first define the function @{text REG}, which takes the statements
+  We define the function @{text REG}, which takes the statements
   of the raw theorem and the lifted theorem (both as terms) and
   returns the statement of the regularized version. The intuition
   behind this function is that it replaces quantifiers and
   abstractions involving raw types by bounded ones, and equalities
   involving raw types are replaced by appropriate aggregate
-  relations. It is defined as follows:
+  equivalence relations. It is defined as follows:
 
   \begin{center}
   \begin{tabular}{rcl}