1.1 --- a/src/HOL/Set.ML	Wed Dec 02 15:52:39 1998 +0100
     1.2 +++ b/src/HOL/Set.ML	Wed Dec 02 15:53:05 1998 +0100
     1.3 @@ -63,10 +63,16 @@
     1.4  claset_ref() := claset() addWrapper ("bspec", fn tac2 =>
     1.5  			 (dtac bspec THEN' atac) APPEND' tac2);
     1.6  
     1.7 +(*Normally the best argument order: P(x) constrains the choice of x:A*)
     1.8  Goalw [Bex_def] "[| P(x);  x:A |] ==> ? x:A. P(x)";
     1.9  by (Blast_tac 1);
    1.10  qed "bexI";
    1.11  
    1.12 +(*The best argument order when there is only one x:A*)
    1.13 +Goalw [Bex_def] "[| x:A;  P(x) |] ==> ? x:A. P(x)";
    1.14 +by (Blast_tac 1);
    1.15 +qed "rev_bexI";
    1.16 +
    1.17  qed_goal "bexCI" Set.thy 
    1.18     "[| ! x:A. ~P(x) ==> P(a);  a:A |] ==> ? x:A. P(x)" (fn prems =>
    1.19    [ (rtac classical 1),