# 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 \ set ys)" by (induct xs) auto -lemma hd_in_set: "l = x#xs \ x\set l" -by (case_tac l, auto) +lemma hd_in_set[simp]: "xs \ [] \ hd xs : set xs" +by(cases xs) auto lemma set_subset_Cons: "set xs \ set (x # xs)" by auto