src/HOL/Fun.thy
changeset 44890 22f665a2e91c
parent 44860 56101fa00193
child 44921 58eef4843641
     1.1 --- a/src/HOL/Fun.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Fun.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -461,7 +461,7 @@
     1.4  lemma surj_vimage_empty:
     1.5    assumes "surj f" shows "f -` A = {} \<longleftrightarrow> A = {}"
     1.6    using surj_image_vimage_eq[OF `surj f`, of A]
     1.7 -  by (intro iffI) fastsimp+
     1.8 +  by (intro iffI) fastforce+
     1.9  
    1.10  lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A"
    1.11  by (simp add: inj_on_def, blast)
    1.12 @@ -603,7 +603,7 @@
    1.13  by (rule ext, auto)
    1.14  
    1.15  lemma inj_on_fun_updI: "\<lbrakk> inj_on f A; y \<notin> f`A \<rbrakk> \<Longrightarrow> inj_on (f(x:=y)) A"
    1.16 -by (fastsimp simp:inj_on_def image_def)
    1.17 +by (fastforce simp:inj_on_def image_def)
    1.18  
    1.19  lemma fun_upd_image:
    1.20       "f(x:=y) ` A = (if x \<in> A then insert y (f ` (A-{x})) else f ` A)"