# HG changeset patch
# User nipkow
# Date 1129044600 -7200
# Node ID 695a2365d32f7699417279ad1a062e8a8bf8f60c
# Parent  35123f89801ec77cd239f0f5caec40bead12e913
added hd lemma

diff -r 35123f89801e -r 695a2365d32f src/HOL/List.thy
--- 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