# HG changeset patch
# User paulson
# Date 936346468 -7200
# Node ID 6dd6110968c9e5007c25a44b194c42844fc02f54
# Parent  ee17ad649c2683690956c15a54667ab3d82de017
new theorem fun_upd_upd

diff -r ee17ad649c26 -r 6dd6110968c9 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Fri Sep 03 10:12:42 1999 +0200
+++ b/src/HOL/Fun.ML	Fri Sep 03 10:14:28 1999 +0200
@@ -300,6 +300,7 @@
 qed "fun_upd_apply";
 Addsimps [fun_upd_apply];
 
+(*fun_upd_apply supersedes these two*)
 Goal "(f(x:=y)) x = y";
 by (Simp_tac 1);
 qed "fun_upd_same";
@@ -308,8 +309,11 @@
 by (Asm_simp_tac 1);
 qed "fun_upd_other";
 
-(*Currently unused?
-  We could try Addsimps [fun_upd_same, fun_upd_other];*)
+Goal "f(x:=y,x:=z) = f(x:=z)";
+by (rtac ext 1);
+by (Simp_tac 1);
+qed "fun_upd_upd";
+Addsimps [fun_upd_upd];
 
 Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)";
 by (rtac ext 1);