# HG changeset patch
# User haftmann
# Date 1324738390 -3600
# Node ID e8fa5090fa04b8b34153311d4ca1400a396f0150
# Parent  76cf71ed15c7b2347ca12c5f9f33801325ec86bb
dropped obsolete lemma member_set

diff -r 76cf71ed15c7 -r e8fa5090fa04 src/HOL/List.thy
--- 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"