--- a/Quotient-Paper/Paper.thy	Thu May 27 16:33:10 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Thu May 27 16:53:12 2010 +0200
@@ -415,21 +415,46 @@
 subsection {* Proof of Regularization *}
 
 text {*
-Example of non-regularizable theorem ($0 = 1$).
+  Example of non-regularizable theorem ($0 = 1$).
+
 
-Separtion of regularization from injection thanks to the following 2 lemmas:
-\begin{lemma}
-If @{term R2} is an equivalence relation, then:
-\begin{eqnarray}
-@{thm (rhs) ball_reg_eqv_range[no_vars]} & = & @{thm (lhs) ball_reg_eqv_range[no_vars]}\\
-@{thm (rhs) bex_reg_eqv_range[no_vars]} & = & @{thm (lhs) bex_reg_eqv_range[no_vars]}
-\end{eqnarray}
-\end{lemma}
+  Separtion of regularization from injection thanks to the following 2 lemmas:
+  \begin{lemma}
+  If @{term R2} is an equivalence relation, then:
+  \begin{eqnarray}
+  @{thm (rhs) ball_reg_eqv_range[no_vars]} & = & @{thm (lhs) ball_reg_eqv_range[no_vars]}\\
+  @{thm (rhs) bex_reg_eqv_range[no_vars]} & = & @{thm (lhs) bex_reg_eqv_range[no_vars]}
+  \end{eqnarray}
+  \end{lemma}
+
+  Other lemmas used in regularization:
+  @{thm [display] ball_reg_eqv[no_vars]}
+  @{thm [display] bex_reg_eqv[no_vars]}
+  @{thm [display] babs_reg_eqv[no_vars]}
+  @{thm [display] babs_simp[no_vars]}
+
+  @{thm [display] ball_reg_right[no_vars]}
+  @{thm [display] bex_reg_left[no_vars]}
+  @{thm [display] bex1_bexeq_reg[no_vars]}
 
 *}
 
 subsection {* Injection *}
 
+text {*
+
+  The 2 key lemmas are:
+
+  @{thm [display] apply_rsp[no_vars]}
+  @{thm [display] rep_abs_rsp[no_vars]}
+
+
+
+*}
+
+
+
+
 subsection {* Cleaning *}
 
 text {* Preservation of quantifiers, abstractions, relations, quotient-constants