src/HOL/Fun.thy
changeset 44921 58eef4843641
parent 44890 22f665a2e91c
child 44928 7ef6505bde7f
     1.1 --- a/src/HOL/Fun.thy	Tue Sep 13 08:21:51 2011 -0700
     1.2 +++ b/src/HOL/Fun.thy	Tue Sep 13 17:07:33 2011 -0700
     1.3 @@ -610,7 +610,7 @@
     1.4  by auto
     1.5  
     1.6  lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
     1.7 -by (auto intro: ext)
     1.8 +  by auto
     1.9  
    1.10  lemma UNION_fun_upd:
    1.11    "UNION J (A(i:=B)) = (UNION (J-{i}) A \<union> (if i\<in>J then B else {}))"