--- a/Quotient-Paper/Paper.thy	Sat Jun 05 14:37:05 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Sun Jun 06 13:16:27 2010 +0200
@@ -527,8 +527,26 @@
 
 subsection {* Cleaning *}
 
-text {* Preservation of quantifiers, abstractions, relations, quotient-constants
-  (definitions) and user given constant preservation lemmas *}
+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.
+
+  \begin{itemize}
+  \item First for lifted constants, their definitions are the preservation rules for
+    them.
+  \item For lambda abstractions lambda preservation establishes
+    the equality between the injected theorem and the goal. This allows both
+    abstraction and quantification over lifted types.
+    @{thm [display] lambda_prs[no_vars]}
+  \item Relations over lifted types are folded with:
+    @{thm [display] Quotient_rel_rep[no_vars]}
+  \item User given preservation theorems, that allow using higher level operations
+    and containers of types being lifted. An example may be
+    @{thm [display] map_prs(1)[no_vars]}
+  \end{itemize}
+
+ Preservation of relations and user given constant preservation lemmas *}
 
 section {* Examples *}