# HG changeset patch # User nipkow # Date 1181463822 -7200 # Node ID b785068bd5dc5b54f28562e7507a494f8a402caa # Parent 292b1cbd05dcc8ec453339bf2bad2c50c759c751 *** empty log message *** diff -r 292b1cbd05dc -r b785068bd5dc NEWS --- a/NEWS Sat Jun 09 02:38:51 2007 +0200 +++ b/NEWS Sun Jun 10 10:23:42 2007 +0200 @@ -31,7 +31,7 @@ these tend to cause confusion about the actual goal (!) context being used here, which is not necessarily the same as the_context(). -* Command 'find_theorems': support "*" wildcard in "name:" criterion. +* Command 'find_theorems': supports "*" wildcard in "name:" criterion. * Proof General interface: A search form for the "Find Theorems" command is now available via C-c C-a C-f. The old minibuffer interface is available @@ -574,6 +574,10 @@ [(x,y). x <- xs, y <- ys, x ~= y] For details see List.thy. +* The special syntax for function "filter" has changed from [x : xs. P] to + [x <- xs. P] to avoid an ambiguity caused by list comprehension syntax, + and for uniformity. INCOMPATIBILITY + * Library/Pretty_Int.thy: maps HOL numerals on target language integer literals when generating code.