diff -r a8299195ed82 -r 5be0b0604d71 NEWS
--- a/NEWS	Thu Aug 17 22:29:30 2017 +0200
+++ b/NEWS	Fri Aug 18 14:57:23 2017 +0200
@@ -121,6 +121,9 @@
 
 *** HOL ***
 
+* Theory Library/Pattern_Aliases provides input syntax for pattern
+aliases as known from Haskell, Scala and ML.
+
 * Constant "subseq" in Topological_Spaces removed and subsumed by
 "strict_mono". Some basic lemmas specific to "subseq" have been renamed
 accordingly, e.g. "subseq_o" -> "strict_mono_o" etc.