--- a/src/HOL/Library/Cardinality.thy Mon Jan 14 18:35:03 2019 +0000
+++ b/src/HOL/Library/Cardinality.thy Tue Jan 15 21:31:20 2019 +0100
@@ -153,6 +153,19 @@
lemma one_le_card_finite [simp]: "Suc 0 \<le> CARD('a::finite)"
by (simp add: less_Suc_eq_le [symmetric])
+
+class CARD_1 =
+ assumes CARD_1: "CARD ('a) = 1"
+begin
+
+subclass finite
+proof
+ from CARD_1 show "finite (UNIV :: 'a set)"
+ by (auto intro!: card_ge_0_finite)
+qed
+
+end
+
text \<open>Class for cardinality "at least 2"\<close>
class card2 = finite +