src/HOL/List.thy
changeset 45968 e8fa5090fa04
parent 45932 6f08f8fe9752
child 45993 3ca49a4bcc9f
--- a/src/HOL/List.thy	Sat Dec 24 15:53:09 2011 +0100
+++ b/src/HOL/List.thy	Sat Dec 24 15:53:10 2011 +0100
@@ -5086,10 +5086,6 @@
   @{prop "x \<in> set xs"} instead --- it is much easier to reason about.
 *}
 
-lemma member_set:
-  "member = set"
-  by (simp add: fun_eq_iff member_def mem_def)
-
 lemma member_rec [code]:
   "member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y"
   "member [] y \<longleftrightarrow> False"