--- a/src/HOL/Library/Numeral_Type.thy Mon Mar 31 23:29:36 2008 +0200
+++ b/src/HOL/Library/Numeral_Type.thy Wed Apr 02 12:32:53 2008 +0200
@@ -8,7 +8,7 @@
header "Numeral Syntax for Types"
theory Numeral_Type
- imports Infinite_Set
+ imports ATP_Linkup
begin
subsection {* Preliminary lemmas *}
@@ -127,7 +127,7 @@
by (simp only: card_prod card_option card_bool)
lemma card_num0: "CARD (num0) = 0"
- by (simp add: type_definition.card [OF type_definition_num0])
+ by (simp add: infinite_UNIV_nat card_eq_0_iff type_definition.card [OF type_definition_num0])
lemmas card_univ_simps [simp] =
card_unit