*** empty log message ***
authornipkow
Sun Jun 10 10:23:42 2007 +0200 (2007-06-10)
changeset 23300b785068bd5dc
parent 23299 292b1cbd05dc
child 23301 4c7e6d295980
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Sat Jun 09 02:38:51 2007 +0200
     1.2 +++ b/NEWS	Sun Jun 10 10:23:42 2007 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  these tend to cause confusion about the actual goal (!) context being
     1.5  used here, which is not necessarily the same as the_context().
     1.6  
     1.7 -* Command 'find_theorems': support "*" wildcard in "name:" criterion.
     1.8 +* Command 'find_theorems': supports "*" wildcard in "name:" criterion.
     1.9  
    1.10  * Proof General interface: A search form for the "Find Theorems" command is
    1.11  now available via C-c C-a C-f.  The old minibuffer interface is available
    1.12 @@ -574,6 +574,10 @@
    1.13    [(x,y). x <- xs, y <- ys, x ~= y]
    1.14    For details see List.thy.
    1.15  
    1.16 +* The special syntax for function "filter" has changed from [x : xs. P] to
    1.17 +  [x <- xs. P] to avoid an ambiguity caused by list comprehension syntax,
    1.18 +  and for uniformity. INCOMPATIBILITY
    1.19 +
    1.20  * Library/Pretty_Int.thy: maps HOL numerals on target language integer literals
    1.21      when generating code.
    1.22