NEWS

--- a/NEWS	Sat Feb 24 17:21:35 2018 +0100
+++ b/NEWS	Sun Feb 25 12:59:08 2018 +0100
@@ -176,6 +176,12 @@
 (e.g. use 'find_theorems' or 'try' to figure this out).
 
 
+*** Pure ***
+
+* The inner syntax category "sort" now includes notation "_" for the
+dummy sort: it is effectively ignored in type-inference.
+
+
 *** HOL ***
 
 * Clarifed theorem names: