--- a/Quotient-Paper/Paper.thy	Wed May 26 16:56:38 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Wed May 26 17:10:05 2010 +0200
@@ -281,16 +281,25 @@
   preservation theorems are needed.
 *}
 
-section {* Lifting Theorems *}
+subsection {* Composition of Quotient theorems *}
 
-text{*
+text {*
+  Given two quotients, one of which quotients a container, and the
+  other quotients the type in the container, we can write the
+  composition of those quotients. This becomes especially interesting
+  when we compose the quotient with itself, as there is no simple
+  intermediate step.
+
+  Lets take again the example of @{term concat}. To 
+
   Aggregate @{term "Rep"} and @{term "Abs"} functions are also
   present in composition quotients. An example composition quotient
   theorem that needs to be proved is the one needed to lift theorems
   about concat:
 
   @{thm [display] quotient_compose_list[no_vars]}
-*}
+
+section {* Lifting Theorems *}
 
 text {* TBD *}