--- a/QuotMain.thy	Sun Dec 06 11:21:29 2009 +0100
+++ b/QuotMain.thy	Sun Dec 06 11:39:34 2009 +0100
@@ -494,14 +494,6 @@
 
 *)
 
-(* FIXME: they should be in in the new Isabelle *)
-lemma [mono]: 
-  "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"
-by blast
-
-lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
-by auto
-
 (* FIXME: OPTION_equivp, PAIR_equivp, ... *)
 ML {*
 fun equiv_tac rel_eqvs =
@@ -511,6 +503,8 @@
      rtac @{thm list_equivp}])
 *}
 
+thm ball_reg_eqv
+
 ML {*
 fun ball_reg_eqv_simproc rel_eqvs ss redex =
   let
@@ -610,6 +604,9 @@
   end
 *}
 
+thm ball_reg_eqv_range
+thm bex_reg_eqv_range
+
 ML {*
 fun bex_reg_eqv_range_simproc rel_eqvs ss redex =
   let