| changeset 5335 | 07fb8999de62 |
| parent 5316 | 7a8975451a89 |
| child 5608 | a82a038a3e7a |
--- 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 ]);