src/HOL/Fun.thy

--- a/src/HOL/Fun.thy	Tue Sep 06 11:31:01 2011 +0200
+++ b/src/HOL/Fun.thy	Tue Sep 06 14:25:16 2011 +0200
@@ -612,6 +612,10 @@
 lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
 by (auto intro: ext)
 
+lemma UNION_fun_upd:
+  "UNION J (A(i:=B)) = (UNION (J-{i}) A \<union> (if i\<in>J then B else {}))"
+by (auto split: if_splits)
+
 
 subsection {* @{text override_on} *}