# HG changeset patch
# User wenzelm
# Date 1321817173 -3600
# Node ID d2d9ef16ccaf723354caa8789dbb2924aa180466
# Parent  2a858377c3d2e2c395136613505087697a115d97
explicit is better than implicit;

diff -r 2a858377c3d2 -r d2d9ef16ccaf src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sun Nov 20 20:15:02 2011 +0100
+++ b/src/HOL/Fun.thy	Sun Nov 20 20:26:13 2011 +0100
@@ -578,12 +578,11 @@
 apply (rule_tac [2] ext, auto)
 done
 
-(* f x = y ==> f(x:=y) = f *)
-lemmas fun_upd_idem = fun_upd_idem_iff [THEN iffD2, standard]
+lemma fun_upd_idem: "f x = y ==> f(x:=y) = f"
+  by (simp only: fun_upd_idem_iff)
 
-(* f(x := f x) = f *)
-lemmas fun_upd_triv = refl [THEN fun_upd_idem]
-declare fun_upd_triv [iff]
+lemma fun_upd_triv [iff]: "f(x := f x) = f"
+  by (simp only: fun_upd_idem)
 
 lemma fun_upd_apply [simp]: "(f(x:=y))z = (if z=x then y else f z)"
 by (simp add: fun_upd_def)