src/HOL/Fun.thy
changeset 31080 21ffc770ebc0
parent 30301 429612400fe9
child 31202 52d332f8f909
     1.1 --- a/src/HOL/Fun.thy	Fri May 08 19:20:00 2009 +0200
     1.2 +++ b/src/HOL/Fun.thy	Sat May 09 07:25:22 2009 +0200
     1.3 @@ -412,6 +412,9 @@
     1.4       "f(x:=y) ` A = (if x \<in> A then insert y (f ` (A-{x})) else f ` A)"
     1.5  by auto
     1.6  
     1.7 +lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
     1.8 +by(auto intro: ext)
     1.9 +
    1.10  
    1.11  subsection {* @{text override_on} *}
    1.12