--- a/Quotient-Paper/Paper.thy	Tue Jun 01 15:58:59 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Wed Jun 02 13:58:37 2010 +0200
@@ -117,8 +117,9 @@
     types. Rsp/Prs extended. (used in nominal)
 
   \item The quotient package is very modular. Definitions can be added
-    separately, rsp and prs can be proved separately and theorems can
-    be lifted on a need basis. (useful with type-classes). 
+    separately, rsp and prs can be proved separately, Quotients and maps
+    can be defined separately and theorems can
+    be lifted on a need basis. (useful with type-classes).
 
   \item Can be used both manually (attribute, separate tactics,
     rsp/prs databases) and programatically (automated definition of
@@ -431,17 +432,22 @@
   \end{eqnarray}
   \end{lemma}
 
+  Monos.
+
   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]}
-
-*}
+  @{thm [display] bex_reg_eqv[no_vars]}
+*)
 
 subsection {* Injection *}
 
@@ -466,6 +472,8 @@
 
 section {* Examples *}
 
+
+
 section {* Related Work *}
 
 text {*