equal
deleted
inserted
replaced
72 |
72 |
73 lemma exists_ex [simp]: |
73 lemma exists_ex [simp]: |
74 "list_ex P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)" |
74 "list_ex P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)" |
75 by (induct xs) auto |
75 by (induct xs) auto |
76 |
76 |
77 class finite = |
77 class finite = type + |
78 fixes fin :: "'a list" |
78 fixes fin :: "'a list" |
79 assumes member_fin: "x \<in> set fin" |
79 assumes member_fin: "x \<in> set fin" |
80 begin |
80 begin |
81 |
81 |
82 lemma set_enum_UNIV: |
82 lemma set_enum_UNIV: |