src/HOL/Finite_Set.thy

   assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
 begin
 
 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]:
   "UNIV = {()}" by auto