No longer imports InfiniteSet, ATP_Linkup is sufficient.
authorchaieb
Wed Apr 02 12:32:53 2008 +0200 (2008-04-02)
changeset 26506c4202c67fe3e
parent 26505 49967f8b1068
child 26507 6da615cef733
No longer imports InfiniteSet, ATP_Linkup is sufficient.
src/HOL/Library/Numeral_Type.thy
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Mon Mar 31 23:29:36 2008 +0200
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Wed Apr 02 12:32:53 2008 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  header "Numeral Syntax for Types"
     1.5  
     1.6  theory Numeral_Type
     1.7 -  imports Infinite_Set
     1.8 +  imports ATP_Linkup
     1.9  begin
    1.10  
    1.11  subsection {* Preliminary lemmas *}
    1.12 @@ -127,7 +127,7 @@
    1.13    by (simp only: card_prod card_option card_bool)
    1.14  
    1.15  lemma card_num0: "CARD (num0) = 0"
    1.16 -  by (simp add: type_definition.card [OF type_definition_num0])
    1.17 +  by (simp add: infinite_UNIV_nat card_eq_0_iff type_definition.card [OF type_definition_num0])
    1.18  
    1.19  lemmas card_univ_simps [simp] =
    1.20    card_unit