1.1 --- a/src/HOL/Library/Binomial.thy	Mon Nov 25 15:56:23 2013 +0100
     1.2 +++ b/src/HOL/Library/Binomial.thy	Mon Nov 25 16:59:02 2013 +0000
     1.3 @@ -91,17 +91,14 @@
     1.4      {s. s \<subseteq> M \<and> card s = Suc k} \<union> {s. \<exists>t. t \<subseteq> M \<and> card t = k \<and> s = insert x t}"
     1.5    apply safe
     1.6       apply (auto intro: finite_subset [THEN card_insert_disjoint])
     1.7 -  apply (drule_tac x = "xa - {x}" in spec)
     1.8 -  by (metis card_Diff_singleton_if card_infinite diff_Suc_1 in_mono insert_Diff_single insert_absorb lessI less_nat_zero_code subset_insert_iff)
     1.9 +  by (metis (full_types) Diff_insert_absorb Set.set_insert Zero_neq_Suc card_Diff_singleton_if 
    1.10 +     card_eq_0_iff diff_Suc_1 in_mono subset_insert_iff)
    1.11  
    1.12  lemma finite_bex_subset [simp]:
    1.13    assumes "finite B"
    1.14      and "\<And>A. A \<subseteq> B \<Longrightarrow> finite {x. P x A}"
    1.15    shows "finite {x. \<exists>A \<subseteq> B. P x A}"
    1.16 -proof -
    1.17 -  have "{x. \<exists>A\<subseteq>B. P x A} = (\<Union>A \<in> Pow B. {x. P x A})" by blast
    1.18 -  with assms show ?thesis by simp
    1.19 -qed
    1.20 +  by (metis (no_types) assms finite_Collect_bounded_ex finite_Collect_subsets)
    1.21  
    1.22  text{*There are as many subsets of @{term A} having cardinality @{term k}
    1.23   as there are sets obtained from the former by inserting a fixed element
    1.24 @@ -259,11 +256,8 @@
    1.25    case False
    1.26    from assms obtain h where "k = Suc h" by (cases k) auto
    1.27    then show ?thesis
    1.28 -    apply (simp add: pochhammer_Suc_setprod)
    1.29 -    apply (rule_tac x="n" in bexI)
    1.30 -    using assms
    1.31 -    apply auto
    1.32 -    done
    1.33 +    by (simp add: pochhammer_Suc_setprod)
    1.34 +       (metis Suc_leI Suc_le_mono assms atLeastAtMost_iff less_eq_nat.simps(1))
    1.35  qed
    1.36  
    1.37  lemma pochhammer_of_nat_eq_0_lemma':
    1.38 @@ -292,8 +286,7 @@
    1.39    apply (auto simp add: pochhammer_of_nat_eq_0_iff)
    1.40    apply (cases n)
    1.41     apply (auto simp add: pochhammer_def algebra_simps group_add_class.eq_neg_iff_add_eq_0)
    1.42 -  apply (rule_tac x=x in exI)
    1.43 -  apply auto
    1.44 +  apply (metis leD not_less_eq)
    1.45    done
    1.46  
    1.47