# HG changeset patch
# User paulson
# Date 903515220 -7200
# Node ID 07fb8999de623adf3468c88d70f391cc13b4ebf0
# Parent  68e5eeee4e599784c79c70284f7f863001667e9f
Overloading decl should assist Blast_tac

diff -r 68e5eeee4e59 -r 07fb8999de62 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Wed Aug 19 10:26:37 1998 +0200
+++ b/src/HOL/Relation.ML	Wed Aug 19 10:27:00 1998 +0200
@@ -174,6 +174,8 @@
 
 (*** Image of a set under a relation ***)
 
+Blast.overloaded ("Relation.op ^^", HOLogic.dest_setT o domain_type);
+
 qed_goalw "Image_iff" thy [Image_def]
     "b : r^^A = (? x:A. (x,b):r)"
  (fn _ => [ Blast_tac 1 ]);