*** empty log message ***
authornipkow
Sun Jun 03 13:19:03 2007 +0200 (2007-06-03)
changeset 23210a0cb15114e7a
parent 23209 098a23702aba
child 23211 4d56ad10b5e8
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Sun Jun 03 12:58:28 2007 +0200
     1.2 +++ b/NEWS	Sun Jun 03 13:19:03 2007 +0200
     1.3 @@ -560,8 +560,9 @@
     1.4  * new function listsum :: 'a list => 'a for arbitrary monoids.
     1.5    Special syntax: "SUM x <- xs. f x" (and latex variants)
     1.6  
     1.7 -* Library/List_Comprehension.thy provides Haskell-like input syntax for list
     1.8 -  comprehensions.
     1.9 +* new (input only) syntax for Haskell-like list comprehension, eg
    1.10 +  [(x,y). x <- xs, y <- ys, x ~= y]
    1.11 +  For details see List.thy.
    1.12  
    1.13  * Library/Pretty_Int.thy: maps HOL numerals on target language integer literals
    1.14      when generating code.