src/HOL/Library/Numeral_Type.thy
changeset 48063 f02b4302d5dd
parent 47108 2a1953f0d20d
child 49834 b27bbb021df1
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Fri Jun 01 08:32:26 2012 +0200
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Fri Jun 01 11:53:58 2012 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  
     1.5  lemma card_num1 [simp]: "CARD(num1) = 1"
     1.6    unfolding type_definition.card [OF type_definition_num1]
     1.7 -  by (simp only: card_unit)
     1.8 +  by (simp only: card_UNIV_unit)
     1.9  
    1.10  lemma card_bit0 [simp]: "CARD('a bit0) = 2 * CARD('a::finite)"
    1.11    unfolding type_definition.card [OF type_definition_bit0]