--- a/Quotient-Paper/Paper.thy	Tue Jun 15 05:43:21 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue Jun 15 06:35:57 2010 +0200
@@ -743,14 +743,15 @@
 section {* Lifting of Theorems\label{sec:lift} *}
 
 text {*
-  The core of our quotient package takes an original theorem that
-  talks about the raw types and the statement of the theorem that
+  The core of our quotient package takes an original theorem
+  involving raw types and a 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
+  an automated statement translation mechanism which can produce
+  the latter automatically given a list of quotient types.
+  It is possible that a user wants
+  to lift only some occurrences of a raw 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
@@ -765,9 +766,7 @@
   can be performed independently from each other.
 
 *}
-
-subsection {* Regularization and Injection statements *}
-
+text {* \textit{Regularization and Injection statements} *}
 text {*
 
   We define the function @{text REG}, which takes the statements
@@ -825,8 +824,7 @@
   defined similarly to the universal one.
 
 *}
-
-subsection {* Proof procedure *}
+text {*\textit{Proof Procedure}*}
 
 (* In the below the type-guiding 'QuotTrue' assumption is removed. We need it
    only for bound variables without types, while in the paper presentation
@@ -859,10 +857,9 @@
   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 *}
-
+text {* \textit{Proving Regularization} *}
 text {*
 
   Isabelle provides a set of \emph{mono} rules, that are used to split implications
@@ -888,8 +885,8 @@
   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.
-
 *}
+text {* \textit{Proving Rep/Abs Injection} *}
 
 (*
   @{thm bex_reg_eqv_range[no_vars]}
@@ -900,8 +897,6 @@
   @{thm [display] babs_simp[no_vars]}
 *)
 
-subsection {* Injection *}
-
 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
@@ -927,10 +922,9 @@
   @{thm [display, indent=10] apply_rsp[no_vars]}
 
 *}
+text {* \textit{Cleaning} *}
+text {*
 
-subsection {* Cleaning *}
-
-text {*
   The @{text REG} and @{text INJ} functions have been defined in such a way
   that establishing the goal theorem now consists only on rewriting the
   injected theorem with the preservation theorems.