diff -r 43da9adf4759 -r 86c73a06ba4b Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Sun Jul 18 17:03:05 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Sun Jul 18 19:07:05 2010 +0100
@@ -822,27 +822,27 @@
 
   \begin{center}
   \begin{tabular}{l@ {\hspace{4mm}}l}
-  1.) Regularisation & @{text "raw_thm \<longrightarrow> reg_thm"}\\
+  1.) Regularization & @{text "raw_thm \<longrightarrow> reg_thm"}\\
   2.) Injection & @{text "reg_thm \<longleftrightarrow> inj_thm"}\\
   3.) Cleaning & @{text "inj_thm \<longleftrightarrow> quot_thm"}\\
   \end{tabular}
   \end{center}
 
   \noindent
-  which means the raw theorem implies the quotient theorem.
-  In contrast to other quotient packages, our package requires
-  the \emph{term} of the @{text "quot_thm"} to be given by the user.\footnote{Though we
+  which means, stringed together, the raw theorem implies the quotient theorem.
+  In contrast to other quotient packages, our package requires that the user specifies 
+  both, the @{text "raw_thm"} (as theorem) and the \emph{term} of the @{text "quot_thm"}.\footnote{Though we
   also provide a fully automated mode, where the @{text "quot_thm"} is guessed
-  from the form of @{text "raw_thm"}.} As a result, it is possible that a user can lift only some
-  occurrences of a raw type, but not others. 
+  from the form of @{text "raw_thm"}.} As a result, the user has fine control
+  over which parts of a raw theorem should be lifted. 
 
-  The second and third proof step will always succeed if the appropriate
+  The second and third proof step performed in package will always succeed if the appropriate
   respectfulness and preservation theorems are given. In contrast, the first
   proof step can fail: a theorem given by the user does not always
   imply a regularized version and a stronger one needs to be proved. An example
   for this kind of failure is the simple statement for integers @{text "0 \<noteq> 1"}.
   One might hope that it can be proved by lifting @{text "(0, 0) \<noteq> (1, 0)"},  
-  but this raw theorem only shows that particular element in the
+  but this raw theorem only shows that two particular elements in the
   equivalence classes are not equal. In order to obtain @{text "0 \<noteq> 1"}, a  
   more general statement stipulating that the equivalence classes are not 
   equal is necessary.  This kind of failure is beyond the scope where the 
@@ -856,14 +856,17 @@
   on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps,
   which can all be performed independently from each other.
 
-  We first define the function @{text REG}. The intuition
+  We first define the function @{text REG}, which takes terms of the 
+  @{text "raw_thm"} and @{text "quot_thm"} as input and returns
+  @{text "reg_thm"}. 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
-  equivalence relations. It is defined as follows:
+  equivalence relations. It is defined by simultaneously recursing on 
+  the structure of  @{text "raw_thm"} and @{text "quot_thm"} as follows:
 
   \begin{center}
-  \begin{longtable}{rcl}
+  \begin{tabular}{rcl}
   \multicolumn{3}{@ {}l}{abstractions:}\smallskip\\
   @{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} & $\dn$ & 
   $\begin{cases}
@@ -883,8 +886,8 @@
   \multicolumn{3}{@ {}l}{applications, variables and constants:}\\
   @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} & $\dn$ & @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\
   @{text "REG (x\<^isub>1, x\<^isub>2)"} & $\dn$ & @{text "x\<^isub>1"}\\
-  @{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\[-5mm]
-  \end{longtable}
+  @{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\
+  \end{tabular}
   \end{center}
   %
   \noindent