changeset 13508 | 890d736b93a5 |
parent 13480 | bb72bd43c6c3 |
child 13585 | db4005b40cc6 |
--- 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} *}