Overloading decl should assist Blast_tac
authorpaulson
Wed Aug 19 10:27:00 1998 +0200 (1998-08-19)
changeset 533507fb8999de62
parent 5334 68e5eeee4e59
child 5336 721bf1a13f1a
Overloading decl should assist Blast_tac
src/HOL/Relation.ML
     1.1 --- a/src/HOL/Relation.ML	Wed Aug 19 10:26:37 1998 +0200
     1.2 +++ b/src/HOL/Relation.ML	Wed Aug 19 10:27:00 1998 +0200
     1.3 @@ -174,6 +174,8 @@
     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 +
     1.9  qed_goalw "Image_iff" thy [Image_def]
    1.10      "b : r^^A = (? x:A. (x,b):r)"
    1.11   (fn _ => [ Blast_tac 1 ]);