# HG changeset patch
# User paulson
# Date 989330488 -7200
# Node ID 65782388cf40a11fa006637fbb1a360129a0dfcd
# Parent  7fe6593133d44e95028e634fff8662365a9a448e
new takeWhile lemma

diff -r 7fe6593133d4 -r 65782388cf40 src/HOL/List.ML
--- a/src/HOL/List.ML	Tue May 08 15:57:13 2001 +0200
+++ b/src/HOL/List.ML	Tue May 08 16:01:28 2001 +0200
@@ -941,6 +941,11 @@
 bind_thm("takeWhile_append2", ballI RS (result() RS mp));
 Addsimps [takeWhile_append2];
 
+Goal "~P(x) ==> takeWhile P (xs @ (x#l)) = takeWhile P xs";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "takeWhile_tail";
+
 Goal "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
 by (induct_tac "xs" 1);
 by Auto_tac;