src/HOL/Library/FinFun.thy
changeset 48100 0122ba071e1a
parent 48070 02d64fd40852
child 49834 b27bbb021df1
     1.1 --- a/src/HOL/Library/FinFun.thy	Mon Jun 04 12:55:54 2012 +0200
     1.2 +++ b/src/HOL/Library/FinFun.thy	Tue Jun 12 15:31:53 2012 +0200
     1.3 @@ -906,6 +906,9 @@
     1.4  lemma expand_finfun_eq: "(f = g) = (op $ f = op $ g)"
     1.5  by(auto intro: finfun_ext)
     1.6  
     1.7 +lemma finfun_upd_triv [simp]: "f(x $:= f $ x) = f"
     1.8 +by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
     1.9 +
    1.10  lemma finfun_const_inject [simp]: "(K$ b) = (K$ b') \<equiv> b = b'"
    1.11  by(simp add: expand_finfun_eq fun_eq_iff)
    1.12