src/HOL/Set.ML
changeset 5521 7970832271cc
parent 5490 85855f65d0c6
child 5600 34b3366b83ac
     1.1 --- a/src/HOL/Set.ML	Mon Sep 21 23:06:37 1998 +0200
     1.2 +++ b/src/HOL/Set.ML	Mon Sep 21 23:12:31 1998 +0200
     1.3 @@ -59,14 +59,16 @@
     1.4  
     1.5  AddSIs [ballI];
     1.6  AddEs  [ballE];
     1.7 +(* gives better instantiation for bound: *)
     1.8 +claset_ref() := claset() addWrapper ("bspec", fn tac2 =>
     1.9 +			 (dtac bspec THEN' atac) APPEND' tac2);
    1.10  
    1.11  Goalw [Bex_def] "[| P(x);  x:A |] ==> ? x:A. P(x)";
    1.12  by (Blast_tac 1);
    1.13  qed "bexI";
    1.14  
    1.15  qed_goal "bexCI" Set.thy 
    1.16 -   "[| ! x:A. ~P(x) ==> P(a);  a:A |] ==> ? x:A. P(x)"
    1.17 - (fn prems=>
    1.18 +   "[| ! x:A. ~P(x) ==> P(a);  a:A |] ==> ? x:A. P(x)" (fn prems =>
    1.19    [ (rtac classical 1),
    1.20      (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1))  ]);
    1.21