src/HOL/Enum.thy
changeset 40683 a3f37b3d303a
parent 40659 b26afaa55a75
child 40898 882e860a1e83
     1.1 --- a/src/HOL/Enum.thy	Wed Nov 24 10:42:28 2010 +0100
     1.2 +++ b/src/HOL/Enum.thy	Wed Nov 24 10:52:02 2010 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  
     1.5  lemma enum_all: "set enum = UNIV" unfolding UNIV_enum ..
     1.6  
     1.7 -lemma in_enum [intro]: "x \<in> set enum"
     1.8 +lemma in_enum: "x \<in> set enum"
     1.9    unfolding enum_all by auto
    1.10  
    1.11  lemma enum_eq_I:
    1.12 @@ -167,9 +167,9 @@
    1.13    proof (rule UNIV_eq_I)
    1.14      fix f :: "'a \<Rightarrow> 'b"
    1.15      have "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
    1.16 -      by (auto simp add: map_of_zip_map fun_eq_iff)
    1.17 +      by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum)
    1.18      then show "f \<in> set enum"
    1.19 -      by (auto simp add: enum_fun_def set_n_lists)
    1.20 +      by (auto simp add: enum_fun_def set_n_lists intro: in_enum)
    1.21    qed
    1.22  next
    1.23    from map_of_zip_enum_inject