src/HOL/List.thy
changeset 13508 890d736b93a5
parent 13480 bb72bd43c6c3
child 13585 db4005b40cc6
     1.1 --- a/src/HOL/List.thy	Sat Aug 17 14:55:08 2002 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Aug 21 15:53:30 2002 +0200
     1.3 @@ -555,6 +555,11 @@
     1.4  lemma in_listsI [intro!]: "\<forall>x\<in>set xs. x \<in> A ==> xs \<in> lists A"
     1.5  by (rule in_lists_conv_set [THEN iffD2])
     1.6  
     1.7 +lemma finite_list: "finite A ==> EX l. set l = A"
     1.8 +apply (erule finite_induct, auto)
     1.9 +apply (rule_tac x="x#l" in exI, auto)
    1.10 +done
    1.11 +
    1.12  
    1.13  subsection {* @{text mem} *}
    1.14