added hd lemma

--- a/src/HOL/List.thy	Tue Oct 11 15:04:11 2005 +0200
+++ b/src/HOL/List.thy	Tue Oct 11 17:30:00 2005 +0200
@@ -637,8 +637,8 @@
 lemma set_append [simp]: "set (xs @ ys) = (set xs \<union> set ys)"
 by (induct xs) auto
 
-lemma hd_in_set: "l = x#xs \<Longrightarrow> x\<in>set l"
-by (case_tac l, auto)
+lemma hd_in_set[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs : set xs"
+by(cases xs) auto
 
 lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)"
 by auto