src/HOL/Set.ML
changeset 5649 1bac26652f45
parent 5600 34b3366b83ac
child 5931 325300576da7
     1.1 --- a/src/HOL/Set.ML	Thu Oct 15 11:35:07 1998 +0200
     1.2 +++ b/src/HOL/Set.ML	Thu Oct 15 11:38:39 1998 +0200
     1.3 @@ -117,12 +117,16 @@
     1.4  by (REPEAT (ares_tac (prems @ [ballI]) 1));
     1.5  qed "subsetI";
     1.6  
     1.7 +(*Map the type ('a set => anything) to just 'a.
     1.8 +  For overloading constants whose first argument has type "'a set" *)
     1.9 +fun overload_1st_set s = Blast.overloaded (s, HOLogic.dest_setT o domain_type);
    1.10 +
    1.11  (*While (:) is not, its type must be kept
    1.12    for overloading of = to work.*)
    1.13  Blast.overloaded ("op :", domain_type);
    1.14 -seq (fn a => Blast.overloaded (a, HOLogic.dest_setT o domain_type))
    1.15 -    ["Ball", "Bex"];
    1.16 -(*need UNION, INTER also?*)
    1.17 +
    1.18 +overload_1st_set "Ball";		(*need UNION, INTER also?*)
    1.19 +overload_1st_set "Bex";
    1.20  
    1.21  (*Image: retain the type of the set being expressed*)
    1.22  Blast.overloaded ("op ``", domain_type);