src/HOL/List.thy

--- a/src/HOL/List.thy	Sat Aug 17 14:55:08 2002 +0200
+++ b/src/HOL/List.thy	Wed Aug 21 15:53:30 2002 +0200
@@ -555,6 +555,11 @@
 lemma in_listsI [intro!]: "\<forall>x\<in>set xs. x \<in> A ==> xs \<in> lists A"
 by (rule in_lists_conv_set [THEN iffD2])
 
+lemma finite_list: "finite A ==> EX l. set l = A"
+apply (erule finite_induct, auto)
+apply (rule_tac x="x#l" in exI, auto)
+done
+
 
 subsection {* @{text mem} *}