# HG changeset patch # User krauss # Date 1185306678 -7200 # Node ID e6d505d5b03d97d82ded5076b0eb07faad17ea57 # Parent a252a7da82b9ec2d287ec1c917ae3d967fe0a3ca renamed lemma "set_take_whileD" to "set_takeWhileD" diff -r a252a7da82b9 -r e6d505d5b03d NEWS --- 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) diff -r a252a7da82b9 -r e6d505d5b03d src/HOL/List.thy --- 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 \ P x" +lemma set_takeWhileD: "x : set (takeWhile P xs) ==> x : set xs \ P x" by (induct xs) (auto split: split_if_asm) lemma takeWhile_eq_all_conv[simp]: