# HG changeset patch
# User bulwahn
# Date 1290592322 -3600
# Node ID a3f37b3d303ada3ffcee4262942652bba5a4e588
# Parent  1e761b5cd09713024004dfefca507aab7302b487
removing Enum.in_enum from the claset

diff -r 1e761b5cd097 -r a3f37b3d303a src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Wed Nov 24 10:42:28 2010 +0100
+++ b/src/HOL/Enum.thy	Wed Nov 24 10:52:02 2010 +0100
@@ -19,7 +19,7 @@
 
 lemma enum_all: "set enum = UNIV" unfolding UNIV_enum ..
 
-lemma in_enum [intro]: "x \<in> set enum"
+lemma in_enum: "x \<in> set enum"
   unfolding enum_all by auto
 
 lemma enum_eq_I:
@@ -167,9 +167,9 @@
   proof (rule UNIV_eq_I)
     fix f :: "'a \<Rightarrow> 'b"
     have "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
-      by (auto simp add: map_of_zip_map fun_eq_iff)
+      by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum)
     then show "f \<in> set enum"
-      by (auto simp add: enum_fun_def set_n_lists)
+      by (auto simp add: enum_fun_def set_n_lists intro: in_enum)
   qed
 next
   from map_of_zip_enum_inject