# HG changeset patch
# User haftmann
# Date 1189877261 -7200
# Node ID c87238132dc37b2bf3ff426f278ed6bae5b8a316
# Parent  c359896d0f48d0cf8fbc5e10394e99b3a114a340
added lemmas for finiteness

diff -r c359896d0f48 -r c87238132dc3 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 +