author | haftmann |
Sat, 24 Dec 2011 15:53:10 +0100 | |
changeset 45968 | e8fa5090fa04 |
parent 45967 | 76cf71ed15c7 |
child 45969 | 562e99c3d316 |
src/HOL/List.thy | file | annotate | diff | comparison | revisions |
--- 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"