# HG changeset patch
# User nipkow
# Date 1128513692 -7200
# Node ID e3cd31bc2e409b820ddbd2390169c5abc7708978
# Parent  fde495b9e24bfaf963f13399bcc71b0f85e61cb9
added last in set lemma

diff -r fde495b9e24b -r e3cd31bc2e40 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Oct 05 11:18:06 2005 +0200
+++ b/src/HOL/List.thy	Wed Oct 05 14:01:32 2005 +0200
@@ -994,13 +994,14 @@
 lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
 by(simp add:last_append)
 
-
 lemma hd_rev: "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
 by(rule rev_exhaust[of xs]) simp_all
 
 lemma last_rev: "xs \<noteq> [] \<Longrightarrow> last(rev xs) = hd xs"
 by(cases xs) simp_all
 
+lemma last_in_set[simp]: "as \<noteq> [] \<Longrightarrow> last as \<in> set as"
+by (induct as) auto
 
 lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
 by (induct xs rule: rev_induct) auto