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