| changeset 24286 | 7619080e49f0 |
| parent 24017 | 363287741ebe |
| child 25886 | 7753e0d81b7a |
--- a/src/HOL/Fun.thy Wed Aug 15 09:02:11 2007 +0200 +++ b/src/HOL/Fun.thy Wed Aug 15 12:52:56 2007 +0200 @@ -268,7 +268,7 @@ lemma vimage_id [simp]: "id -` A = A" by (simp add: id_def) -lemma vimage_image_eq: "f -` (f ` A) = {y. EX x:A. f x = f y}" +lemma vimage_image_eq [noatp]: "f -` (f ` A) = {y. EX x:A. f x = f y}" by (blast intro: sym) lemma image_vimage_subset: "f ` (f -` A) <= A"