summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

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 | file | annotate | diff | comparison | revisions |

--- 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