Corected bug in def of dropWhile (also present in Haskell lib!)
authornipkow
Fri, 01 Aug 1997 09:42:19 +0200
changeset 3584 8f9ee0f79d9a
parent 3583 5a47b869d16a
child 3585 5b2dcdc1829c
Corected bug in def of dropWhile (also present in Haskell lib!)
src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Aug 01 09:41:38 1997 +0200
+++ b/src/HOL/List.thy	Fri Aug 01 09:42:19 1997 +0200
@@ -108,7 +108,7 @@
   "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
 primrec dropWhile list
   "dropWhile P [] = []"
-  "dropWhile P (x#xs) = (if P x then dropWhile P xs else xs)"
+  "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
 
 end