# 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