--- a/src/HOL/Enum.thy Mon Jun 25 16:03:14 2012 +0200
+++ b/src/HOL/Enum.thy Mon Jun 25 16:03:21 2012 +0200
@@ -784,10 +784,14 @@
subsection {* Further operations on finite types *}
-lemma [code]:
+lemma Collect_code[code]:
"Collect P = set (filter P enum)"
by (auto simp add: enum_UNIV)
+lemma [code]:
+ "Id = image (%x. (x, x)) (set Enum.enum)"
+by (auto intro: imageI in_enum)
+
lemma tranclp_unfold [code, no_atp]:
"tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
by (simp add: trancl_def)