changeset 47221 | 7205eb4a0a05 |
parent 47108 | 2a1953f0d20d |
child 48051 | 53a0df441e20 |
--- a/src/HOL/Library/Cardinality.thy Fri Mar 30 12:32:35 2012 +0200 +++ b/src/HOL/Library/Cardinality.thy Fri Mar 30 14:00:18 2012 +0200 @@ -59,7 +59,7 @@ lemma card_set [simp]: "CARD('a set) = 2 ^ CARD('a::finite)" unfolding Pow_UNIV [symmetric] - by (simp only: card_Pow finite numeral_2_eq_2) + by (simp only: card_Pow finite) lemma card_nat [simp]: "CARD(nat) = 0" by (simp add: card_eq_0_iff)