# HG changeset patch # User wenzelm # Date 1469005867 -7200 # Node ID f8213afea07f2575f6fd3b178d4d90bff249061c # Parent 54e932f0c30a298a1c2257cc37a1b24b430b65ad unused (see also 651ea265d568); diff -r 54e932f0c30a -r f8213afea07f src/HOL/Binomial.thy --- a/src/HOL/Binomial.thy Tue Jul 19 16:50:39 2016 +0200 +++ b/src/HOL/Binomial.thy Wed Jul 20 11:11:07 2016 +0200 @@ -1424,18 +1424,6 @@ lemma choose_one: "n choose 1 = n" for n :: nat by simp -(*FIXME: messy and apparently unused*) -lemma binomial_induct [rule_format]: "(\n::nat. P n n) \ - (\n. P (Suc n) 0) \ (\n. (\k < n. P n k \ P n (Suc k) \ - P (Suc n) (Suc k))) \ (\k \ n. P n k)" - apply (induct n) - apply auto - apply (case_tac "k = 0") - apply auto - apply (case_tac "k = Suc n") - apply (auto simp add: le_Suc_eq elim: lessE) - done - lemma card_UNION: assumes "finite A" and "\k \ A. finite k"