src/HOL/Finite_Set.thy

   thus ?thesis by blast
 qed
 
 lemma finite_Collect_less_nat [iff]:
   "finite {n::nat. n < k}"
-  by (fastsimp simp: finite_conv_nat_seg_image)
+  by (fastforce simp: finite_conv_nat_seg_image)
 
 lemma finite_Collect_le_nat [iff]:
   "finite {n::nat. n \<le> k}"
   by (simp add: le_eq_less_or_eq Collect_disj_eq)
 

   show ?thesis
   proof (intro exI conjI)
     show "A = insert b (A-{b})" using b by blast
     show "b \<notin> A - {b}" by blast
     show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
-      using assms b fin by(fastsimp dest:mk_disjoint_insert)+
+      using assms b fin by(fastforce dest:mk_disjoint_insert)+
   qed
 qed
 
 lemma card_Suc_eq:
   "(card A = Suc k) =

  apply(auto intro:ccontr)
 done
 
 lemma card_le_Suc_iff: "finite A \<Longrightarrow>
   Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)"
-by (fastsimp simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff
+by (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff
   dest: subset_singletonD split: nat.splits if_splits)
 
 lemma finite_fun_UNIVD2:
   assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
   shows "finite (UNIV :: 'b set)"

 shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
 by (blast intro: finite_surj_inj subset_UNIV)
 
 lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
 shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
-by(fastsimp simp:surj_def dest!: endo_inj_surj)
+by(fastforce simp:surj_def dest!: endo_inj_surj)
 
 corollary infinite_UNIV_nat[iff]: "~finite(UNIV::nat set)"
 proof
   assume "finite(UNIV::nat set)"
   with finite_UNIV_inj_surj[of Suc]