src/ZF/pair.thy
 changeset 42455 6702c984bf5a parent 41777 1f7cbe39d425 child 42456 13b4b6ba3593
```--- 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 @@

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 **)
```