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