src/HOL/Relation.ML
changeset 5649 1bac26652f45
parent 5608 a82a038a3e7a
child 5811 0867068942e6
     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)"