# HG changeset patch
# User wenzelm
# Date 1128718755 -7200
# Node ID 407bea05c2da76500d3c16e94132d817cb3e5a30
# Parent  93d7e524417a2174b788fcc891abbbb2ac786b51
added dummy variable binding;
removed obsolete _K;

diff -r 93d7e524417a -r 407bea05c2da NEWS
--- a/NEWS	Fri Oct 07 20:41:10 2005 +0200
+++ b/NEWS	Fri Oct 07 22:59:15 2005 +0200
@@ -9,6 +9,18 @@
 * Command 'find_theorems': support "*" wildcard in "name:" criterion.
 
 
+*** Pure ***
+
+* Input syntax now supports dummy variable binding "%_. b", where the
+body does not mention the bound variable.  Note that dummy patterns
+implicitly depend on their context of bounds, which makes "{_. _}"
+match any set comprehension as expected.
+
+* Removed obsolete syntactic constant _K and its associated parse
+translation.  INCOMPATIBILITY, use dummy abstraction instead, for
+example "A -> B" => "Pi A (%_. B)".
+
+
 
 New in Isabelle2005 (October 2005)
 ----------------------------------