# HG changeset patch
# User paulson
# Date 912610385 -3600
# Node ID d2e271b8d651a2e86434b4cde7e56944d37ea089
# Parent  45186ec4d8b6587e3cc037adfe4f1addf343f65e
new rule rev_bexI

diff -r 45186ec4d8b6 -r d2e271b8d651 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Wed Dec 02 15:52:39 1998 +0100
+++ b/src/HOL/Set.ML	Wed Dec 02 15:53:05 1998 +0100
@@ -63,10 +63,16 @@
 claset_ref() := claset() addWrapper ("bspec", fn tac2 =>
 			 (dtac bspec THEN' atac) APPEND' tac2);
 
+(*Normally the best argument order: P(x) constrains the choice of x:A*)
 Goalw [Bex_def] "[| P(x);  x:A |] ==> ? 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) |] ==> ? x:A. P(x)";
+by (Blast_tac 1);
+qed "rev_bexI";
+
 qed_goal "bexCI" Set.thy 
    "[| ! x:A. ~P(x) ==> P(a);  a:A |] ==> ? x:A. P(x)" (fn prems =>
   [ (rtac classical 1),