src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Sat Sep 15 19:27:40 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Sat Sep 15 19:27:41 2007 +0200
@@ -2679,7 +2679,11 @@
 end
 
 
-subsection {* Class @{text finite} *}
+subsection {* Class @{text finite} and code generation *}
+
+lemma finite_code [code func]:
+  "finite {} \<longleftrightarrow> True"
+  "finite (insert a A) \<longleftrightarrow> finite A" by auto
 
 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
 class finite (attach UNIV) = type +