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"