--- a/src/HOL/Library/Cardinality.thy Thu Jun 28 09:16:00 2012 +0200
+++ b/src/HOL/Library/Cardinality.thy Thu Jun 28 09:18:58 2012 +0200
@@ -208,6 +208,12 @@
instance by intro_classes (simp add: card_UNIV_int_def infinite_UNIV_int)
end
+instantiation code_numeral :: card_UNIV begin
+definition "card_UNIV = Phantom(code_numeral) 0"
+instance
+ by(intro_classes)(auto simp add: card_UNIV_code_numeral_def type_definition.univ[OF type_definition_code_numeral] card_eq_0_iff dest!: finite_imageD intro: inj_onI)
+end
+
instantiation list :: (type) card_UNIV begin
definition "card_UNIV = Phantom('a list) 0"
instance by intro_classes (simp add: card_UNIV_list_def infinite_UNIV_listI)
@@ -223,6 +229,11 @@
instance by(intro_classes)(simp add: card_UNIV_bool_def card_UNIV_bool)
end
+instantiation nibble :: card_UNIV begin
+definition "card_UNIV = Phantom(nibble) 16"
+instance by(intro_classes)(simp add: card_UNIV_nibble_def card_nibble)
+end
+
instantiation char :: card_UNIV begin
definition "card_UNIV = Phantom(char) 256"
instance by intro_classes (simp add: card_UNIV_char_def card_UNIV_char)