author | paulson |
Wed, 19 Aug 1998 10:27:00 +0200 | |
changeset 5335 | 07fb8999de62 |
parent 5334 | 68e5eeee4e59 |
child 5336 | 721bf1a13f1a |
--- 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 ]);