--- 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