src/HOL/Library/FinFun.thy
changeset 58787 af9eb5e566dd
parent 55565 f663fc1e653b
child 58881 b9556a055632
     1.1 --- a/src/HOL/Library/FinFun.thy	Sat Oct 25 19:20:28 2014 +0200
     1.2 +++ b/src/HOL/Library/FinFun.thy	Sun Oct 26 19:11:16 2014 +0100
     1.3 @@ -890,7 +890,7 @@
     1.4  by(simp add: finfun_upd_apply)
     1.5  
     1.6  lemma finfun_ext: "(\<And>a. f $ a = g $ a) \<Longrightarrow> f = g"
     1.7 -by(auto simp add: finfun_apply_inject[symmetric] simp del: finfun_apply_inject)
     1.8 +by(auto simp add: finfun_apply_inject[symmetric])
     1.9  
    1.10  lemma expand_finfun_eq: "(f = g) = (op $ f = op $ g)"
    1.11  by(auto intro: finfun_ext)
    1.12 @@ -1287,7 +1287,7 @@
    1.13  lemma finfun_dom_update [simp]:
    1.14    "finfun_dom (f(a $:= b)) = (finfun_dom f)(a $:= (b \<noteq> finfun_default f))"
    1.15  including finfun unfolding finfun_dom_def finfun_update_def
    1.16 -apply(simp add: finfun_default_update_const fun_upd_apply finfun_dom_finfunI)
    1.17 +apply(simp add: finfun_default_update_const finfun_dom_finfunI)
    1.18  apply(fold finfun_update.rep_eq)
    1.19  apply(simp add: finfun_upd_apply fun_eq_iff fun_upd_def finfun_default_update_const)
    1.20  done
    1.21 @@ -1495,7 +1495,7 @@
    1.22      thus "finite (UNIV :: 'b set)"
    1.23        by(rule finite_imageD)(auto intro!: inj_onI)
    1.24    qed
    1.25 -  with False show ?thesis by simp
    1.26 +  with False show ?thesis by auto
    1.27  qed
    1.28  
    1.29  lemma finite_UNIV_finfun: