--- 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