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/Library/Finite_Map.thy
changeset 69313 b021008c5397
parent 69142 c5e3212455ed
child 69593 3dda49e08b9d 
--- a/src/HOL/Library/Finite_Map.thy	Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Library/Finite_Map.thy	Sun Nov 18 18:07:51 2018 +0000
@@ -818,7 +818,7 @@
   by (rule rel_funI ext)+ (auto simp: fmap.Abs_fmap_inverse fmap.pcr_cr_eq cr_fmap_def)
 
 lemma fmran'_transfer[transfer_rule]:
-  "(pcr_fmap (=) (=) ===> (=)) (\<lambda>x. UNION (range x) set_option) fmran'"
+  "(pcr_fmap (=) (=) ===> (=)) (\<lambda>x. \<Union>(set_option ` (range x))) fmran'"
   unfolding fmran'_def fmap.pcr_cr_eq cr_fmap_def by fastforce
 
 lemma fmrel_transfer[transfer_rule]:
isabelle