src/HOL/Library/Numeral_Type.thy

--- a/src/HOL/Library/Numeral_Type.thy	Mon Jan 14 18:35:03 2019 +0000
+++ b/src/HOL/Library/Numeral_Type.thy	Tue Jan 15 21:31:20 2019 +0100
@@ -52,6 +52,16 @@
     using finite by (rule finite_imageI)
 qed
 
+instantiation num1 :: CARD_1
+begin
+
+instance
+proof
+  show "CARD(num1) = 1" by auto
+qed
+
+end
+
 instance bit0 :: (finite) card2
 proof
   show "finite (UNIV::'a bit0 set)"