explicit is better than implicit;
authorwenzelm
Sun Nov 20 20:26:13 2011 +0100 (2011-11-20)
changeset 45603d2d9ef16ccaf
parent 45602 2a858377c3d2
child 45604 29cf40fe8daf
explicit is better than implicit;
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.thy	Sun Nov 20 20:15:02 2011 +0100
     1.2 +++ b/src/HOL/Fun.thy	Sun Nov 20 20:26:13 2011 +0100
     1.3 @@ -578,12 +578,11 @@
     1.4  apply (rule_tac [2] ext, auto)
     1.5  done
     1.6  
     1.7 -(* f x = y ==> f(x:=y) = f *)
     1.8 -lemmas fun_upd_idem = fun_upd_idem_iff [THEN iffD2, standard]
     1.9 +lemma fun_upd_idem: "f x = y ==> f(x:=y) = f"
    1.10 +  by (simp only: fun_upd_idem_iff)
    1.11  
    1.12 -(* f(x := f x) = f *)
    1.13 -lemmas fun_upd_triv = refl [THEN fun_upd_idem]
    1.14 -declare fun_upd_triv [iff]
    1.15 +lemma fun_upd_triv [iff]: "f(x := f x) = f"
    1.16 +  by (simp only: fun_upd_idem)
    1.17  
    1.18  lemma fun_upd_apply [simp]: "(f(x:=y))z = (if z=x then y else f z)"
    1.19  by (simp add: fun_upd_def)