src/HOL/Set.thy
changeset 27418 564117b58d73
parent 27106 ff27dc6e7d05
child 27824 97d2a3797ce0
     1.1 --- a/src/HOL/Set.thy	Tue Jul 01 06:21:28 2008 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Jul 01 06:51:59 2008 +0200
     1.3 @@ -1324,7 +1324,7 @@
     1.4  lemma full_SetCompr_eq [noatp]: "{u. \<exists>x. u = f x} = range f"
     1.5    by auto
     1.6  
     1.7 -lemma range_composition [simp]: "range (\<lambda>x. f (g x)) = f`range g"
     1.8 +lemma range_composition: "range (\<lambda>x. f (g x)) = f`range g"
     1.9  by (subst image_image, simp)
    1.10  
    1.11