# HG changeset patch # User nipkow # Date 1180109456 -7200 # Node ID 559709b43104cfb77a3ddadad8c7aca7c66ace3c # Parent 1a05d89feeaf895535a2516ba7769fe3a1bc7cda *** empty log message *** diff -r 1a05d89feeaf -r 559709b43104 NEWS --- a/NEWS Fri May 25 18:08:47 2007 +0200 +++ b/NEWS Fri May 25 18:10:56 2007 +0200 @@ -550,6 +550,9 @@ * new class "default" with associated constant "default" +* Library/List_Comprehension provides Haskell-like input syntax for list + comprehensions. + * Library/Pretty_Int.thy: maps HOL numerals on target language integer literals when generating code.