| changeset 5649 | 1bac26652f45 |
| parent 5608 | a82a038a3e7a |
| child 5811 | 0867068942e6 |
--- a/src/HOL/Relation.ML Thu Oct 15 11:35:07 1998 +0200 +++ b/src/HOL/Relation.ML Thu Oct 15 11:38:39 1998 +0200 @@ -174,7 +174,7 @@ (*** Image of a set under a relation ***) -Blast.overloaded ("Relation.op ^^", HOLogic.dest_setT o domain_type); +overload_1st_set "Relation.op ^^"; qed_goalw "Image_iff" thy [Image_def] "b : r^^A = (? x:A. (x,b):r)"