--- a/src/HOL/Library/Binomial.thy Fri May 15 10:01:57 2009 +0200
+++ b/src/HOL/Library/Binomial.thy Sat May 16 11:28:02 2009 +0200
@@ -88,9 +88,7 @@
lemma card_s_0_eq_empty:
"finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
- apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
- apply (simp cong add: rev_conj_cong)
- done
+by (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
lemma choose_deconstruct: "finite M ==> x \<notin> M
==> {s. s <= insert x M & card(s) = Suc k}