diff -r 804dfa6d35b6 -r bdf8eb8f126b 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 \ (g(x := y)) = (f \ g)(x := f y)" by (auto intro: ext) +lemma UNION_fun_upd: + "UNION J (A(i:=B)) = (UNION (J-{i}) A \ (if i\J then B else {}))" +by (auto split: if_splits) + subsection {* @{text override_on} *}