# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1274887259 -7200
# Node ID aae246e2a5dc54dad740fc90e4237e58cca8698a
# Parent  87024a9a9d8938055a4f0c3724b89cf2a19d7549
merged

diff -r 87024a9a9d89 -r aae246e2a5dc Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Wed May 26 17:19:16 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Wed May 26 17:20:59 2010 +0200
@@ -286,16 +286,20 @@
 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
+  composition of those quotients. To compose two quotient theorems
+  we compose the relations with relation composition
+  and the abstraction and relation functions with function composition.
+  The @{term "Rep"} and @{term "Abs"} functions that we obtain are
+  the same as the ones created by in the aggregate functions and the
+  relation is the same as the one given by aggregate relations.
+  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:
+  Lets take again the example of @{term concat}. To be able to lift
+  theorems that talk about it we will first prove the composition
+  quotient theorems, which then lets us perform the lifting procedure
+  in an unchanged way:
 
   @{thm [display] quotient_compose_list[no_vars]}
 *}
@@ -303,6 +307,8 @@
 
 section {* Lifting Theorems *}
 
+
+
 text {* TBD *}
 
 text {* Why providing a statement to prove is necessary is some cases *}