changeset 23971 | e6d505d5b03d |
parent 23740 | d7f18c837ce7 |
child 23983 | 79dc793bec43 |
--- a/src/HOL/List.thy Tue Jul 24 20:34:11 2007 +0200 +++ b/src/HOL/List.thy Tue Jul 24 21:51:18 2007 +0200 @@ -1410,7 +1410,7 @@ "(!!x. x:set xs ==> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys" by (induct xs) auto -lemma set_take_whileD: "x : set (takeWhile P xs) ==> x : set xs \<and> P x" +lemma set_takeWhileD: "x : set (takeWhile P xs) ==> x : set xs \<and> P x" by (induct xs) (auto split: split_if_asm) lemma takeWhile_eq_all_conv[simp]: