| changeset 44142 | 8e27e0177518 |
| parent 42247 | 12fe41a92cd5 |
| child 47108 | 2a1953f0d20d |
--- a/src/HOL/Library/Cardinality.thy Wed Aug 10 17:02:03 2011 -0700 +++ b/src/HOL/Library/Cardinality.thy Wed Aug 10 18:02:16 2011 -0700 @@ -62,7 +62,7 @@ by (simp only: card_Pow finite numeral_2_eq_2) lemma card_nat [simp]: "CARD(nat) = 0" - by (simp add: infinite_UNIV_nat card_eq_0_iff) + by (simp add: card_eq_0_iff) subsection {* Classes with at least 1 and 2 *}