1.1 --- a/src/HOL/Library/Enum.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/Library/Enum.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  class enum = itself +
     1.6    fixes enum :: "'a list"
     1.7 -  assumes UNIV_enum [code func]: "UNIV = set enum"
     1.8 +  assumes UNIV_enum [code]: "UNIV = set enum"
     1.9      and enum_distinct: "distinct enum"
    1.10  begin
    1.11  
    1.12 @@ -49,7 +49,7 @@
    1.13  
    1.14  end
    1.15  
    1.16 -lemma order_fun [code func]:
    1.17 +lemma order_fun [code]:
    1.18    fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
    1.19    shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
    1.20      and "f < g \<longleftrightarrow> f \<le> g \<and> \<not> list_all (\<lambda>x. f x = g x) enum"
    1.21 @@ -58,10 +58,10 @@
    1.22  
    1.23  subsection {* Quantifiers *}
    1.24  
    1.25 -lemma all_code [code func]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
    1.26 +lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
    1.27    by (simp add: list_all_iff enum_all)
    1.28  
    1.29 -lemma exists_code [code func]: "(\<exists>x. P x) \<longleftrightarrow> \<not> list_all (Not o P) enum"
    1.30 +lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> \<not> list_all (Not o P) enum"
    1.31    by (simp add: list_all_iff enum_all)
    1.32  
    1.33  
    1.34 @@ -157,7 +157,7 @@
    1.35  begin
    1.36  
    1.37  definition
    1.38 -  [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)"
    1.39 +  [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)"
    1.40  
    1.41  instance proof
    1.42    show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
    1.43 @@ -177,7 +177,7 @@
    1.44  
    1.45  end
    1.46  
    1.47 -lemma enum_fun_code [code func]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list)
    1.48 +lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list)
    1.49    in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
    1.50    by (simp add: enum_fun_def Let_def)
    1.51  
    1.52 @@ -286,9 +286,9 @@
    1.53  begin
    1.54  
    1.55  definition
    1.56 -  [code func del]: "enum = map (split Char) (product enum enum)"
    1.57 +  [code del]: "enum = map (split Char) (product enum enum)"
    1.58  
    1.59 -lemma enum_char [code func]:
    1.60 +lemma enum_char [code]:
    1.61    "enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
    1.62    Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
    1.63    Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,