--- 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)
----------------------------------