--- a/src/HOL/Library/Enum.thy Wed Nov 11 21:53:58 2009 +0100
+++ b/src/HOL/Library/Enum.thy Thu Nov 12 15:10:24 2009 +0100
@@ -10,7 +10,7 @@
class enum =
fixes enum :: "'a list"
- assumes UNIV_enum [code]: "UNIV = set enum"
+ assumes UNIV_enum: "UNIV = set enum"
and enum_distinct: "distinct enum"
begin
@@ -114,10 +114,6 @@
by (simp add: length_n_lists)
qed
-lemma map_of_zip_map: (*FIXME move to Map.thy*)
- "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
- by (induct xs) (simp_all add: expand_fun_eq)
-
lemma map_of_zip_enum_is_Some:
assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y"