# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1274886605 -7200
# Node ID 8fdfbec542292a2031b2b2dc0deeb4ae54f51101
# Parent  0aeb0ea71ef194c5e7e41c4dd018fe4640a6ccbb
qpaper / composition of quotients.

diff -r 0aeb0ea71ef1 -r 8fdfbec54229 Quotient-Paper/Paper.thy
--- 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 *}