src/ZF/pair.thy

--- a/src/ZF/pair.thy	Fri Apr 22 13:07:47 2011 +0200
+++ b/src/ZF/pair.thy	Fri Apr 22 13:58:13 2011 +0200
@@ -7,7 +7,29 @@
 header{*Ordered Pairs*}
 
 theory pair imports upair
-uses "simpdata.ML" begin
+uses "simpdata.ML"
+begin
+
+simproc_setup defined_Bex ("EX x:A. P(x) & Q(x)") = {*
+  let
+    val unfold_bex_tac = unfold_tac @{thms Bex_def};
+    fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
+  in
+    fn _ => fn ss => fn ct =>
+      Quantifier1.rearrange_bex prove_bex_tac (theory_of_cterm ct) ss (term_of ct)
+  end
+*}
+
+simproc_setup defined_Ball ("ALL x:A. P(x) --> Q(x)") = {*
+  let
+    val unfold_ball_tac = unfold_tac @{thms Ball_def};
+    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
+  in
+    fn _ => fn ss => fn ct =>
+      Quantifier1.rearrange_ball prove_ball_tac (theory_of_cterm ct) ss (term_of ct)
+  end
+*}
+
 
 (** Lemmas for showing that <a,b> uniquely determines a and b **)