src/HOL/Library/Enum.thy

 
 subsection {* Class @{text enum} *}
 
 class enum = itself +
   fixes enum :: "'a list"
-  assumes UNIV_enum [code func]: "UNIV = set enum"
+  assumes UNIV_enum [code]: "UNIV = set enum"
     and enum_distinct: "distinct enum"
 begin
 
 lemma finite_enum: "finite (UNIV \<Colon> 'a set)"
   unfolding UNIV_enum ..

 instance by default
   (simp_all add: eq_fun_def enum_all expand_fun_eq)
 
 end
 
-lemma order_fun [code func]:
+lemma order_fun [code]:
   fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
   shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
     and "f < g \<longleftrightarrow> f \<le> g \<and> \<not> list_all (\<lambda>x. f x = g x) enum"
   by (simp_all add: list_all_iff enum_all expand_fun_eq le_fun_def less_fun_def order_less_le)
 
 
 subsection {* Quantifiers *}
 
-lemma all_code [code func]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
+lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
   by (simp add: list_all_iff enum_all)
 
-lemma exists_code [code func]: "(\<exists>x. P x) \<longleftrightarrow> \<not> list_all (Not o P) enum"
+lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> \<not> list_all (Not o P) enum"
   by (simp add: list_all_iff enum_all)
 
 
 subsection {* Default instances *}
 

 
 instantiation "fun" :: (enum, enum) enum
 begin
 
 definition
-  [code func del]: "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
+  [code del]: "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
 
 instance proof
   show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
   proof (rule UNIV_eq_I)
     fix f :: "'a \<Rightarrow> 'b"

       distinct_map distinct_n_lists enum_distinct set_n_lists enum_all)
 qed
 
 end
 
-lemma enum_fun_code [code func]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list)
+lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list)
   in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
   by (simp add: enum_fun_def Let_def)
 
 instantiation unit :: enum
 begin

 
 instantiation char :: enum
 begin
 
 definition
-  [code func del]: "enum = map (split Char) (product enum enum)"
-
-lemma enum_char [code func]:
+  [code del]: "enum = map (split Char) (product enum enum)"
+
+lemma enum_char [code]:
   "enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
   Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
   Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
   Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB,
   Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,