# HG changeset patch # User bulwahn # Date 1327481434 -3600 # Node ID 2ddc00f8ad7cdbf0e7f19ee3fc9bfbf8dd54fa97 # Parent cf3b387ba66769920b8dd33f4dc38528bf1e9872# Parent fd21bbcbe61b32ca3798cb51389919fcacfa5eaa merged diff -r fd21bbcbe61b -r 2ddc00f8ad7c src/HOL/Enum.thy --- a/src/HOL/Enum.thy Tue Jan 24 16:00:51 2012 +0100 +++ b/src/HOL/Enum.thy Wed Jan 25 09:50:34 2012 +0100 @@ -776,11 +776,16 @@ unfolding enum_the_def by (auto split: list.split) qed +code_abort enum_the + +subsection {* Further operations on finite types *} + +lemma [code]: + "Collect P = set (filter P enum)" +by (auto simp add: enum_UNIV) subsection {* Closing up *} -code_abort enum_the - hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5