# HG changeset patch
# User bulwahn
# Date 1291362047 -3600
# Node ID 4d0f96a54e769ae47bc54e58844fb45eaaa9855b
# Parent  a516fbdd9931814496802c0bd1a91aafa7612d71
adding code equation for finiteness of finite types

diff -r a516fbdd9931 -r 4d0f96a54e76 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Dec 03 08:40:47 2010 +0100
@@ -517,6 +517,9 @@
 lemma finite [simp]: "finite (A \<Colon> 'a set)"
   by (rule subset_UNIV finite_UNIV finite_subset)+
 
+lemma finite_code [code]: "finite (A \<Colon> 'a set) = True"
+  by simp
+
 end
 
 lemma UNIV_unit [no_atp]: