--- a/src/HOL/Library/Enum.thy Tue Feb 03 19:48:06 2009 +0100
+++ b/src/HOL/Library/Enum.thy Tue Feb 03 21:26:21 2009 +0100
@@ -11,14 +11,14 @@
subsection {* Class @{text enum} *}
-class enum = itself +
+class enum =
fixes enum :: "'a list"
assumes UNIV_enum [code]: "UNIV = set enum"
and enum_distinct: "distinct enum"
begin
-lemma finite_enum: "finite (UNIV \<Colon> 'a set)"
- unfolding UNIV_enum ..
+subclass finite proof
+qed (simp add: UNIV_enum)
lemma enum_all: "set enum = UNIV" unfolding UNIV_enum ..