# HG changeset patch
# User chaieb
# Date 1207132373 -7200
# Node ID c4202c67fe3e16b9f59402ec2b5d2888a444921a
# Parent  49967f8b1068bdf35e35c5a82dc5a8a9016437cc
No longer imports InfiniteSet, ATP_Linkup is sufficient.

diff -r 49967f8b1068 -r c4202c67fe3e src/HOL/Library/Numeral_Type.thy
--- 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