dropped obsolete lemma member_set
authorhaftmann
Sat, 24 Dec 2011 15:53:10 +0100
changeset 45968 e8fa5090fa04
parent 45967 76cf71ed15c7
child 45969 562e99c3d316
dropped obsolete lemma member_set
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"