1.1 --- a/src/HOL/List.thy	Sat Dec 24 15:53:09 2011 +0100
     1.2 +++ b/src/HOL/List.thy	Sat Dec 24 15:53:10 2011 +0100
     1.3 @@ -5086,10 +5086,6 @@
     1.4    @{prop "x \<in> set xs"} instead --- it is much easier to reason about.
     1.5  *}
     1.6  
     1.7 -lemma member_set:
     1.8 -  "member = set"
     1.9 -  by (simp add: fun_eq_iff member_def mem_def)
    1.10 -
    1.11  lemma member_rec [code]:
    1.12    "member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y"
    1.13    "member [] y \<longleftrightarrow> False"