Added a take/dropWhile lemma.

--- a/src/HOL/List.ML	Fri Aug 01 10:59:19 1997 +0200
+++ b/src/HOL/List.ML	Mon Aug 04 11:50:35 1997 +0200
@@ -571,8 +571,14 @@
 
 section "takeWhile & dropWhile";
 
-goal thy
-  "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
+goal thy "takeWhile P xs @ dropWhile P xs = xs";
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+qed "takeWhile_dropWhile_id";
+Addsimps [takeWhile_dropWhile_id];
+
+goal thy  "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
 by (induct_tac "xs" 1);
  by (Simp_tac 1);
 by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);