diff -r 2382876c238b -r 6383440f41a8 NEWS
--- a/NEWS	Sat Mar 05 19:14:04 2016 +0100
+++ b/NEWS	Sat Mar 05 19:58:56 2016 +0100
@@ -23,6 +23,10 @@
 
 *** HOL ***
 
+* The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@"
+has been removed for output. It is retained for input only, until it is
+eliminated altogether.
+
 * (Co)datatype package:
   - the predicator :: ('a => bool) => 'a F => bool is now a first-class
     citizen in bounded natural functors