Uses overload_1st_set to specify overloading
authorpaulson
Thu Oct 15 11:38:39 1998 +0200 (1998-10-15)
changeset 56491bac26652f45
parent 5648 fe887910e32e
child 5650 38bda28c68a2
Uses overload_1st_set to specify overloading
src/HOL/Relation.ML
src/HOL/Set.ML
     1.1 --- a/src/HOL/Relation.ML	Thu Oct 15 11:35:07 1998 +0200
     1.2 +++ b/src/HOL/Relation.ML	Thu Oct 15 11:38:39 1998 +0200
     1.3 @@ -174,7 +174,7 @@
     1.4  
     1.5  (*** Image of a set under a relation ***)
     1.6  
     1.7 -Blast.overloaded ("Relation.op ^^", HOLogic.dest_setT o domain_type);
     1.8 +overload_1st_set "Relation.op ^^";
     1.9  
    1.10  qed_goalw "Image_iff" thy [Image_def]
    1.11      "b : r^^A = (? x:A. (x,b):r)"
     2.1 --- a/src/HOL/Set.ML	Thu Oct 15 11:35:07 1998 +0200
     2.2 +++ b/src/HOL/Set.ML	Thu Oct 15 11:38:39 1998 +0200
     2.3 @@ -117,12 +117,16 @@
     2.4  by (REPEAT (ares_tac (prems @ [ballI]) 1));
     2.5  qed "subsetI";
     2.6  
     2.7 +(*Map the type ('a set => anything) to just 'a.
     2.8 +  For overloading constants whose first argument has type "'a set" *)
     2.9 +fun overload_1st_set s = Blast.overloaded (s, HOLogic.dest_setT o domain_type);
    2.10 +
    2.11  (*While (:) is not, its type must be kept
    2.12    for overloading of = to work.*)
    2.13  Blast.overloaded ("op :", domain_type);
    2.14 -seq (fn a => Blast.overloaded (a, HOLogic.dest_setT o domain_type))
    2.15 -    ["Ball", "Bex"];
    2.16 -(*need UNION, INTER also?*)
    2.17 +
    2.18 +overload_1st_set "Ball";		(*need UNION, INTER also?*)
    2.19 +overload_1st_set "Bex";
    2.20  
    2.21  (*Image: retain the type of the set being expressed*)
    2.22  Blast.overloaded ("op ``", domain_type);