| changeset 3960 | 7a38fae985f9 |
| parent 3919 | c036caebfc75 |
| child 4059 | 59c1422c9da5 |
--- a/src/HOL/Set.ML Mon Oct 20 17:21:54 1997 +0200 +++ b/src/HOL/Set.ML Tue Oct 21 10:36:23 1997 +0200 @@ -623,6 +623,10 @@ by (Blast_tac 1); qed "image_Un"; +goal Set.thy "(z : f``A) = (EX x:A. z = f x)"; +by (Blast_tac 1); +qed "image_iff"; + (*** Range of a function -- just a translation for image! ***)