1.1 --- a/src/HOL/Fun.ML	Fri Sep 03 10:12:42 1999 +0200
     1.2 +++ b/src/HOL/Fun.ML	Fri Sep 03 10:14:28 1999 +0200
     1.3 @@ -300,6 +300,7 @@
     1.4  qed "fun_upd_apply";
     1.5  Addsimps [fun_upd_apply];
     1.6  
     1.7 +(*fun_upd_apply supersedes these two*)
     1.8  Goal "(f(x:=y)) x = y";
     1.9  by (Simp_tac 1);
    1.10  qed "fun_upd_same";
    1.11 @@ -308,8 +309,11 @@
    1.12  by (Asm_simp_tac 1);
    1.13  qed "fun_upd_other";
    1.14  
    1.15 -(*Currently unused?
    1.16 -  We could try Addsimps [fun_upd_same, fun_upd_other];*)
    1.17 +Goal "f(x:=y,x:=z) = f(x:=z)";
    1.18 +by (rtac ext 1);
    1.19 +by (Simp_tac 1);
    1.20 +qed "fun_upd_upd";
    1.21 +Addsimps [fun_upd_upd];
    1.22  
    1.23  Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)";
    1.24  by (rtac ext 1);