--- a/Quotient-Paper/Paper.thy	Mon Jun 14 15:16:42 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 14 16:44:53 2010 +0200
@@ -676,10 +676,15 @@
 
   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:
+  theorem:
+
+  @{thm [display, indent=10] quotient_compose_list[no_vars]}
 
-  @{thm [display] quotient_compose_list[no_vars]}
+  \noindent
+  this theorem will then instantiate the quotients needed in the
+  injection and cleaning proofs allowing the lifting procedure to
+  proceed in an unchanged way.
+
 *}
 
 
@@ -696,7 +701,6 @@
   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 HOL4
@@ -743,7 +747,6 @@
   In the above definition we omitted the cases for existential quantifiers
   and unique existential quantifiers, as they are very similar to the cases
   for the universal quantifier.
-
   Next we define the function @{text INJ} which takes the statement of
   the regularized theorems and the statement of the lifted theorem both as
   terms and returns the statement of the injected theorem:
@@ -779,13 +782,12 @@
 
 text {*
 
-  With the above definitions of @{text "REG"} and @{text "INJ"} we can show
-  how the proof is performed. The first step is always the application of
-  of the following lemma:
+  When lifting a theorem we first apply the following rule
 
   @{term [display, indent=10] "[|A; A --> B; B = C; C = D|] ==> D"}
 
-  With @{text A} instantiated to the original raw theorem, 
+  \noindent
+  with @{text A} instantiated to the original raw theorem, 
        @{text B} instantiated to @{text "REG(A)"},
        @{text C} instantiated to @{text "INJ(REG(A))"},
    and @{text D} instantiated to the statement of the lifted theorem.
@@ -1007,7 +1009,7 @@
 
 
   The code of the quotient package described here is already included in the
-  standard distribution of Isabelle.\footnote{Avaiable from
+  standard distribution of Isabelle.\footnote{Available from
   \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is
   heavily used in Nominal Isabelle, which provides a convenient reasoning
   infrastructure for programming language calculi involving binders.  Earlier