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/Option.thy
changeset 69275 9bbd5497befd
parent 68460 b047339bd11c 
--- a/src/HOL/Option.thy	Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Option.thy	Sat Nov 10 07:57:19 2018 +0000
@@ -260,7 +260,7 @@
 lemma bind_map_option: "bind (map_option f x) g = bind x (g \<circ> f)"
 by(cases x) simp_all
 
-lemma set_bind_option [simp]: "set_option (bind x f) = UNION (set_option x) (set_option \<circ> f)"
+lemma set_bind_option [simp]: "set_option (bind x f) = (\<Union>((set_option \<circ> f) ` set_option x))"
 by(cases x) auto
 
 lemma map_conv_bind_option: "map_option f x = Option.bind x (Some \<circ> f)"
isabelle