Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Set.thy
changeset 27418 564117b58d73
parent 27106 ff27dc6e7d05
child 27824 97d2a3797ce0 
--- a/src/HOL/Set.thy	Tue Jul 01 06:21:28 2008 +0200
+++ b/src/HOL/Set.thy	Tue Jul 01 06:51:59 2008 +0200
@@ -1324,7 +1324,7 @@
 lemma full_SetCompr_eq [noatp]: "{u. \<exists>x. u = f x} = range f"
   by auto
 
-lemma range_composition [simp]: "range (\<lambda>x. f (g x)) = f`range g"
+lemma range_composition: "range (\<lambda>x. f (g x)) = f`range g"
 by (subst image_image, simp)
isabelle