AddXDs [bspec];
authorwenzelm
Thu Sep 02 15:24:31 1999 +0200 (1999-09-02)
changeset 744120b3e2d2fcb6
parent 7440 c1829208180f
child 7442 2d2849258e3f
AddXDs [bspec];
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Thu Sep 02 15:24:00 1999 +0200
     1.2 +++ b/src/HOL/Set.ML	Thu Sep 02 15:24:31 1999 +0200
     1.3 @@ -57,6 +57,7 @@
     1.4  
     1.5  AddSIs [ballI];
     1.6  AddEs  [ballE];
     1.7 +AddXDs [bspec];
     1.8  (* gives better instantiation for bound: *)
     1.9  claset_ref() := claset() addWrapper ("bspec", fn tac2 =>
    1.10  			 (dtac bspec THEN' atac) APPEND' tac2);