# HG changeset patch
# User paulson
# Date 919675019 -3600
# Node ID 61904a3eafaa8e9b9cd0c35f178bc89a5d9e4449
# Parent  ce30e19af3df6746beb478d201bc4339069b27be
added rev_bexI

diff -r ce30e19af3df -r 61904a3eafaa src/ZF/ZF.ML
--- a/src/ZF/ZF.ML	Thu Feb 18 12:15:55 1999 +0100
+++ b/src/ZF/ZF.ML	Mon Feb 22 10:16:59 1999 +0100
@@ -62,9 +62,14 @@
 
 (*** Bounded existential quantifier ***)
 
-qed_goalw "bexI" ZF.thy [Bex_def]
-    "!!P. [| P(x);  x: A |] ==> EX x:A. P(x)"
- (fn _=> [ Blast_tac 1 ]);
+Goalw [Bex_def] "[| P(x);  x: A |] ==> EX x:A. P(x)";
+by (Blast_tac 1);
+qed "bexI";
+
+(*The best argument order when there is only one x:A*)
+Goalw [Bex_def] "[| x:A;  P(x) |] ==> EX x:A. P(x)";
+by (Blast_tac 1);
+qed "rev_bexI";
 
 (*Not of the general form for such rules; ~EX has become ALL~ *)
 qed_goal "bexCI" ZF.thy