diff -r 1d43f86f48be -r e96292f32c3c NEWS
--- a/NEWS	Mon Dec 28 19:23:15 2015 +0100
+++ b/NEWS	Mon Dec 28 21:47:32 2015 +0100
@@ -375,6 +375,11 @@
 
 *** HOL ***
 
+* Former "xsymbols" syntax with Isabelle symbols is used by default,
+without any special print mode. Important ASCII replacement syntax
+remains available under print mode "ASCII", but less important syntax
+has been removed (see below).
+
 * Combinator to represent case distinction on products is named "case_prod",
 uniformly, discontinuing any input aliasses.  Very popular theorem aliasses
 have been retained.