--- a/src/HOL/Binomial.thy Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Binomial.thy Fri Sep 25 14:11:48 2020 +0100
@@ -81,11 +81,11 @@
proof -
from \<open>n \<in> K\<close> obtain L where "K = insert n L" and "n \<notin> L"
by (blast elim: Set.set_insert)
- with that show ?thesis by (simp add: card_insert)
+ with that show ?thesis by (simp add: card.insert_remove)
qed
show "K \<in> ?A \<longleftrightarrow> K \<in> ?B"
by (subst in_image_insert_iff)
- (auto simp add: card_insert subset_eq_atLeast0_lessThan_finite
+ (auto simp add: card.insert_remove subset_eq_atLeast0_lessThan_finite
Diff_subset_conv K_finite Suc_card_K)
qed
also have "{K\<in>?Q. n \<notin> K} = ?P n (Suc k)"