src/HOL/Library/Cardinality.thy
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)