| changeset 13550 | 5a176b8dda84 |
| parent 13343 | 3b2b18c58d80 |
| child 13639 | 8ee6ea6627e1 |
--- a/src/HOL/Relation.thy Thu Aug 29 16:15:11 2002 +0200 +++ b/src/HOL/Relation.thy Fri Aug 30 16:42:45 2002 +0200 @@ -300,8 +300,6 @@ subsection {* Image of a set under a relation *} -ML {* overload_1st_set "Relation.Image" *} - lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)" by (simp add: Image_def)