--- a/NEWS Tue Jul 24 20:34:11 2007 +0200
+++ b/NEWS Tue Jul 24 21:51:18 2007 +0200
@@ -754,6 +754,8 @@
[x <- xs. P] to avoid an ambiguity caused by list comprehension syntax,
and for uniformity. INCOMPATIBILITY
+* Lemma "set_take_whileD" renamed to "set_takeWhileD"
+
* New lemma collection field_simps (an extension of ring_simps)
for manipulating (in)equations involving division. Multiplies
with all denominators that can be proved to be non-zero (in equations)
--- 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]: