diff -r b0b2198040d7 -r 5952b0f28261 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Sat Jun 05 07:26:22 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Sat Jun 05 08:02:39 2010 +0200
@@ -464,34 +464,38 @@
 subsection {* Proving Regularization *}
 
 text {*
-  Isabelle provides 
-
-
 
-  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}
+  Isabelle provides a set of \emph{mono} rules, that are used to split implications
+  of similar statements into simpler implication subgoals. These are enchanced
+  with special quotient theorem in the regularization goal. Below we only show
+  the versions for the universal quantifier. For the existential quantifier
+  and abstraction they are analoguous with some symmetry.
 
-  Monos.
-
-  Other lemmas used in regularization:
-  @{thm [display] ball_reg_eqv[no_vars]}
-  @{thm [display] babs_reg_eqv[no_vars]}
-  @{thm [display] babs_simp[no_vars]}
+  First, bounded universal quantifiers can be removed on the right:
 
   @{thm [display] ball_reg_right[no_vars]}
 
+  They can be removed anywhere if the relation is an equivalence relation:
+
+  @{thm [display] ball_reg_eqv[no_vars]}
+
+  And finally it can be removed anywhere if @{term R2} is an equivalence relation, then:
+  \[
+  @{thm (rhs) ball_reg_eqv_range[no_vars]} = @{thm (lhs) ball_reg_eqv_range[no_vars]}
+  \]
+
+  The last theorem is new in comparison with Homeier's package; it allows separating
+  regularization from injection.
+
 *}
 
 (*
+  @{thm (rhs) bex_reg_eqv_range[no_vars]} = @{thm (lhs) bex_reg_eqv_range[no_vars]}
   @{thm [display] bex_reg_left[no_vars]}
   @{thm [display] bex1_bexeq_reg[no_vars]}
   @{thm [display] bex_reg_eqv[no_vars]}
+  @{thm [display] babs_reg_eqv[no_vars]}
+  @{thm [display] babs_simp[no_vars]}
 *)
 
 subsection {* Injection *}