equal
deleted
inserted
replaced
57 apply fast |
57 apply fast |
58 done |
58 done |
59 |
59 |
60 lemma card_set [simp]: "CARD('a set) = 2 ^ CARD('a::finite)" |
60 lemma card_set [simp]: "CARD('a set) = 2 ^ CARD('a::finite)" |
61 unfolding Pow_UNIV [symmetric] |
61 unfolding Pow_UNIV [symmetric] |
62 by (simp only: card_Pow finite numeral_2_eq_2) |
62 by (simp only: card_Pow finite) |
63 |
63 |
64 lemma card_nat [simp]: "CARD(nat) = 0" |
64 lemma card_nat [simp]: "CARD(nat) = 0" |
65 by (simp add: card_eq_0_iff) |
65 by (simp add: card_eq_0_iff) |
66 |
66 |
67 |
67 |